src/Doc/ProgProve/Isar.thy

 (*<*)
 theory Isar
 imports LaTeXsugar
 begin
-ML{* quick_and_dirty := true *}
+declare [[quick_and_dirty]]
 (*>*)
 text{*
 Apply-scripts are unreadable and hard to maintain. The language of choice
 for larger proofs is \concept{Isar}. The two key features of Isar are:
 \begin{itemize}