# HG changeset patch
# User wenzelm
# Date 1427122481 -3600
# Node ID 5d801eff5647bff27ad359f27ca25bebdffac0e7
# Parent  a71dbf3481a2035b454347e4bba47117a5be6303
tuned;

diff -r a71dbf3481a2 -r 5d801eff5647 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 14:56:52 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 15:54:41 2015 +0100
@@ -485,7 +485,7 @@
 
   \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
 
@@ -508,7 +508,7 @@
   mode: an assumption is only used for simplifying assumptions which
   are to the right of it \\\hline
 
-  \end{supertabular}
+  \end{tabular}
   \end{center}
 \<close>
 
@@ -1002,11 +1002,10 @@
   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