src/Doc/Isar_Ref/Generic.thy

   follows.\footnote{Unlike the corresponding Isar proof methods, the
   ML tactics do not insist in changing the goal state.}
 
   \begin{center}
   \small
-  \begin{supertabular}{|l|l|p{0.3\textwidth}|}
+  \begin{tabular}{|l|l|p{0.3\textwidth}|}
   \hline
   Isar method & ML tactic & behavior \\\hline
 
   @{text "(simp (no_asm))"} & @{ML simp_tac} & assumptions are ignored
   completely \\\hline

 
   @{text "(simp (asm_lr))"} & @{ML asm_lr_simp_tac} & compatibility
   mode: an assumption is only used for simplifying assumptions which
   are to the right of it \\\hline
 
-  \end{supertabular}
+  \end{tabular}
   \end{center}
 \<close>
 
 
 subsubsection \<open>Examples\<close>

   control over rule application, beyond higher-order pattern matching.
   Declaring @{thm unit_eq} as @{attribute simp} directly would make
   the Simplifier loop!  Note that a version of this simplification
   procedure is already active in Isabelle/HOL.\<close>
 
-simproc_setup unit ("x::unit") = \<open>
-  fn _ => fn _ => fn ct =>
+simproc_setup unit ("x::unit") =
+  \<open>fn _ => fn _ => fn ct =>
     if HOLogic.is_unit (Thm.term_of ct) then NONE
-    else SOME (mk_meta_eq @{thm unit_eq})
-\<close>
+    else SOME (mk_meta_eq @{thm unit_eq})\<close>
 
 text \<open>Since the Simplifier applies simplification procedures
   frequently, it is important to make the failure check in ML
   reasonably fast.\<close>