\documentclass[]{article}{}

% Colored text
\usepackage[dvipsnames]{xcolor}

% Code listings
\usepackage{listings}
\definecolor{isarblue}{HTML}{0040B0}
\definecolor{isarlightblue}{HTML}{6080B0}
\definecolor{isargreen}{HTML}{00A040}
\definecolor{isarred}{HTML}{C00000}
\definecolor{hlred}{HTML}{C09090}
\lstdefinelanguage{isabelle}{%
    keywords=[1]{type_synonym,datatype,fun,abbreviation,definition,
        proof,lemma,theorem,corollary,context,locale,class,qed,next,
        if,then,else,by,using,thus,have,finally,show,hence,
        from,unfolding},
    keywordstyle=[1]\bfseries\color{isarblue},
    keywords=[2]{where,assumes,shows,and,fixes,is,begin,end,assume,obtain,notation,infix},
    keywordstyle=[2]\bfseries\color{isargreen},
    keywords=[3]{case,of,SOME,let,in,O},
    keywordstyle=[3]\color{isarblue},
    keywords=[4]{apply,apply_end},
    keywordstyle=[4]\color{isarred},
    keywords=[5]{moreover,ultimately,also,finally},
    keywordstyle=[5]\color{isarblue},
    keywords=[6]{sorry},
    keywordstyle=[6]\color{isarblue}\colorbox{hlred},
    morecomment=[s]{(*}{*)},
    commentstyle=\color{isarred}\ttfamily,
    extendedchars,
    basicstyle=\footnotesize\ttfamily,
    mathescape
}

\begin{document}
\begin{lstlisting}[language=Isabelle]
notation times (infix "$\odot$" 80)

lemma times_assoc:
    fixes a::r and b::r and c::r
    shows "(a $\odot$ b) $\odot$  c =  a $\odot$ (b $\odot$ c)"
    sorry
\end{lstlisting}
\end{document}