# HG changeset patch
# User wenzelm
# Date 1413839848 -7200
# Node ID 42398b610f865c1699949e756defd44caefb70d5
# Parent  e3d0a6a012eb05c287df4fc7817eb85e318739aa
tuned spacing;

diff -r e3d0a6a012eb -r 42398b610f86 src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Mon Oct 20 22:46:17 2014 +0200
+++ b/src/Doc/Implementation/Isar.thy	Mon Oct 20 23:17:28 2014 +0200
@@ -165,10 +165,9 @@
 notepad
 begin
   have A and B and C
-    ML_val \<open>
-      val n = Thm.nprems_of (#goal @{Isar.goal});
-      @{assert} (n = 3);
-\<close>
+    ML_val
+     \<open>val n = Thm.nprems_of (#goal @{Isar.goal});
+      @{assert} (n = 3);\<close>
     oops
 
 text \<open>Here we see 3 individual subgoals in the same way as regular
diff -r e3d0a6a012eb -r 42398b610f86 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Mon Oct 20 22:46:17 2014 +0200
+++ b/src/Doc/Implementation/Logic.thy	Mon Oct 20 23:17:28 2014 +0200
@@ -981,9 +981,7 @@
 theorem (in empty) false: False
   using bad by blast
 
-ML \<open>
-  @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])
-\<close>
+ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
 
 text \<open>Thanks to the inference kernel managing sort hypothesis
   according to their logical significance, this example is merely an
diff -r e3d0a6a012eb -r 42398b610f86 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Mon Oct 20 22:46:17 2014 +0200
+++ b/src/Doc/Implementation/Proof.thy	Mon Oct 20 23:17:28 2014 +0200
@@ -202,16 +202,15 @@
 
 notepad
 begin
-  ML_prf %"ML" \<open>
-    val ctxt0 = @{context};
+  ML_prf %"ML"
+   \<open>val ctxt0 = @{context};
 
     val ([x1], ctxt1) = ctxt0 |> Variable.add_fixes ["x"];
     val ([x2], ctxt2) = ctxt1 |> Variable.add_fixes ["x"];
     val ([x3], ctxt3) = ctxt2 |> Variable.add_fixes ["x"];
 
     val ([y1, y2], ctxt4) =
-      ctxt3 |> Variable.variant_fixes ["y", "y"];
-\<close>
+      ctxt3 |> Variable.variant_fixes ["y", "y"];\<close>
 end
 
 text \<open>In this situation @{ML Variable.add_fixes} and @{ML
@@ -459,13 +458,11 @@
 
   have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
     ML_val
-    \<open>
-      val {goal, context = goal_ctxt, ...} = @{Isar.goal};
+     \<open>val {goal, context = goal_ctxt, ...} = @{Isar.goal};
       val (focus as {params, asms, concl, ...}, goal') =
         Subgoal.focus goal_ctxt 1 goal;
       val [A, B] = #prems focus;
-      val [(_, x)] = #params focus;
-\<close>
+      val [(_, x)] = #params focus;\<close>
     oops
 
 text \<open>\medskip The next example demonstrates forward-elimination in
@@ -475,18 +472,15 @@
 begin
   assume ex: "\<exists>x. B x"
 
-  ML_prf %"ML" \<open>
-    val ctxt0 = @{context};
+  ML_prf %"ML"
+   \<open>val ctxt0 = @{context};
     val (([(_, x)], [B]), ctxt1) = ctxt0
-      |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];
-\<close>
-  ML_prf %"ML" \<open>
-    singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};
-\<close>
-  ML_prf %"ML" \<open>
-    Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]
-      handle ERROR msg => (warning msg; []);
-\<close>
+      |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];\<close>
+  ML_prf %"ML"
+   \<open>singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\<close>
+  ML_prf %"ML"
+   \<open>Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]
+      handle ERROR msg => (warning msg; []);\<close>
 end
 
 end