% Isabelle
\usepackage{isabelle,isabellesym}
\isabellestyle{literalunderscore}
% Isabelle does not like *} in a text {* ... *} block
% Concrete implemenation thanks to http://www.mrunix.de/forums/showpost.php?p=235085&postcount=5
\newenvironment{alignstar}{\csname align*\endcsname}{\csname endalign*\endcsname}
\newenvironment{alignatstar}{\csname alignat*\endcsname}{\csname endalignat*\endcsname}
% hack to avoid meta quantifiers
\renewcommand{\isasymAnd}{\isasymforall}
% quench koma warnings
\def\bf{\normalfont\bfseries}
\def\it{\normalfont\itshape}
\def\rm{\normalfont}

\newenvironment{isablock}%
  {\vspace{\abovedisplayskip}\begin{isabellebody}}%
  {\end{isabellebody}\vspace{\belowdisplayskip}}

\gdef\lastthy{}%
\newcommand{\thyrefstyle}{\upshape\footnotesize\sffamily}
\newcommand{\thyref}[1]{%
  \ifthenelse{\equal{#1}{\lastthy}}{}{%
    \nointerlineskip%
    \noindent%
    \adjustbox{valign=B, margin=0px, margin=0px, right, raise={-\baselineskip-.5pt}{0px}{0px}}{{\thyrefstyle#1.thy}}%
    \gdef\lastthy{#1}%
    \nopagebreak%
  }
}

\newenvironment{isablocksource}[1]{%
  %\newcommand{\isablocksourcetmp}{#1}
  %\marginpar{#1}
  \vspace{\abovedisplayskip}%
  \par%
  \thyref{#1}%
  \begin{isabellebody}%
  %\smash{}%
}{%
  \end{isabellebody}%
  %\nopagebreak%
  %\adjustbox{right, raise={0px}{\belowdisplayskip}{0px}}{\footnotesize\ttfamily\isablocksourcetmp.thy}%
  \vspace{\belowdisplayskip}%
}
\newcommand{\isainput}[1]{
  \input{isa-thy-output/#1.tex}%
}
\newcommand{\isainputanonym}[1]{
  \renewcommand\thyref[1]{}%
  \input{isa-thy-output/#1.tex}%
}