explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;
\documentclass[11pt,a4paper]{article}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
\isabellestyle{it}
\usepackage{pdfsetup}\urlstyle{rm}
\renewcommand{\isamarkupheader}[1]{\section{#1}}
\renewcommand{\isacommand}[1]
{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
{\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
\newcommand{\dummyproof}{$\DUMMYPROOF$}
\newcommand{\name}[1]{\textsl{#1}}
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
\newcommand{\var}[1]{{?\!\idt{#1}}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\dshsym}
\newcommand{\To}{\to}
\newcommand{\dt}{{\mathpunct.}}
\newcommand{\ap}{\mathbin{\!}}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
\newcommand{\all}[1]{\forall #1\dt\;}
\newcommand{\ex}[1]{\exists #1\dt\;}
\newcommand{\impl}{\to}
\newcommand{\conj}{\land}
\newcommand{\disj}{\lor}
\newcommand{\Impl}{\Longrightarrow}
\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: