# HG changeset patch
# User wenzelm
# Date 1446679033 -3600
# Node ID c49a8ebd30ccc946a9a3630e0ac847a34fbc8a21
# Parent  634cd44bb1d3dd13baae8beb239c3143e1556c61
isabelle update_cartouches -c;

diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -249,16 +249,16 @@
 \<close>
 
     lemmas [intros] =
-      conjI  --  \<open>@{thm conjI}\<close>
-      impI  --  \<open>@{thm impI}\<close>
-      disjCI  --  \<open>@{thm disjCI}\<close>
-      iffI  --  \<open>@{thm iffI}\<close>
-      notI  --  \<open>@{thm notI}\<close>
+      conjI  \<comment>  \<open>@{thm conjI}\<close>
+      impI  \<comment>  \<open>@{thm impI}\<close>
+      disjCI  \<comment>  \<open>@{thm disjCI}\<close>
+      iffI  \<comment>  \<open>@{thm iffI}\<close>
+      notI  \<comment>  \<open>@{thm notI}\<close>
 
     lemmas [elims] =
-      impCE  --  \<open>@{thm impCE}\<close>
-      conjE  --  \<open>@{thm conjE}\<close>
-      disjE  --  \<open>@{thm disjE}\<close>
+      impCE  \<comment>  \<open>@{thm impCE}\<close>
+      conjE  \<comment>  \<open>@{thm conjE}\<close>
+      disjE  \<comment>  \<open>@{thm disjE}\<close>
 
     lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
       by prop_solver
diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Implementation/ML.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -578,7 +578,7 @@
   ML_prf %"ML" \<open>val a = 1\<close>
   {
     ML_prf %"ML" \<open>val b = a + 1\<close>
-  } -- \<open>Isar block structure ignored by ML environment\<close>
+  } \<comment> \<open>Isar block structure ignored by ML environment\<close>
   ML_prf %"ML" \<open>val c = b + 1\<close>
 end
 
diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Implementation/Prelim.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -471,17 +471,17 @@
 begin
 
 declare [[show_types = false]]
-  -- \<open>declaration within (local) theory context\<close>
+  \<comment> \<open>declaration within (local) theory context\<close>
 
 notepad
 begin
   note [[show_types = true]]
-    -- \<open>declaration within proof (forward mode)\<close>
+    \<comment> \<open>declaration within proof (forward mode)\<close>
   term x
 
   have "x = x"
     using [[show_types = false]]
-      -- \<open>declaration within proof (backward mode)\<close>
+      \<comment> \<open>declaration within proof (backward mode)\<close>
     ..
 end
 
diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Implementation/Proof.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -58,14 +58,14 @@
 notepad
 begin
   {
-    fix x  -- \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
+    fix x  \<comment> \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
     {
-      have "x::'a \<equiv> x"  -- \<open>implicit type assignment by concrete occurrence\<close>
+      have "x::'a \<equiv> x"  \<comment> \<open>implicit type assignment by concrete occurrence\<close>
         by (rule reflexive)
     }
-    thm this  -- \<open>result still with fixed type \<open>'a\<close>\<close>
+    thm this  \<comment> \<open>result still with fixed type \<open>'a\<close>\<close>
   }
-  thm this  -- \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
+  thm this  \<comment> \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
 end
 
 text \<open>The Isabelle/Isar proof context manages the details of term
diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Isar_Ref/First_Order_Logic.thy
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -357,10 +357,10 @@
 theorem
   assumes "\<exists>x. \<forall>y. R x y"
   shows "\<forall>y. \<exists>x. R x y"
-proof    -- \<open>\<open>\<forall>\<close> introduction\<close>
-  obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> ..    -- \<open>\<open>\<exists>\<close> elimination\<close>
-  fix y have "R x y" using \<open>\<forall>y. R x y\<close> ..    -- \<open>\<open>\<forall>\<close> destruction\<close>
-  then show "\<exists>x. R x y" ..    -- \<open>\<open>\<exists>\<close> introduction\<close>
+proof    \<comment> \<open>\<open>\<forall>\<close> introduction\<close>
+  obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> ..    \<comment> \<open>\<open>\<exists>\<close> elimination\<close>
+  fix y have "R x y" using \<open>\<forall>y. R x y\<close> ..    \<comment> \<open>\<open>\<forall>\<close> destruction\<close>
+  then show "\<exists>x. R x y" ..    \<comment> \<open>\<open>\<exists>\<close> introduction\<close>
 qed
 
 
diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Isar_Ref/Synopsis.thy
--- a/src/Doc/Isar_Ref/Synopsis.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Isar_Ref/Synopsis.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -17,11 +17,11 @@
 notepad
 begin
   txt \<open>Locally fixed entities:\<close>
-  fix x   -- \<open>local constant, without any type information yet\<close>
-  fix x :: 'a  -- \<open>variant with explicit type-constraint for subsequent use\<close>
+  fix x   \<comment> \<open>local constant, without any type information yet\<close>
+  fix x :: 'a  \<comment> \<open>variant with explicit type-constraint for subsequent use\<close>
 
   fix a b
-  assume "a = b"  -- \<open>type assignment at first occurrence in concrete term\<close>
+  assume "a = b"  \<comment> \<open>type assignment at first occurrence in concrete term\<close>
 
   txt \<open>Definitions (non-polymorphic):\<close>
   def x \<equiv> "t::'a"
@@ -234,7 +234,7 @@
   proof -
     term ?thesis
     show ?thesis sorry
-    term ?thesis  -- \<open>static!\<close>
+    term ?thesis  \<comment> \<open>static!\<close>
   qed
   term "\<dots>"
   thm this
@@ -345,7 +345,7 @@
   moreover
   { assume C have R sorry }
   ultimately
-  have R by blast  -- \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
+  have R by blast  \<comment> \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
 end
 
 
@@ -364,7 +364,7 @@
 begin
   fix n :: nat
   have "P n"
-  proof (rule nat.induct)  -- \<open>fragile rule application!\<close>
+  proof (rule nat.induct)  \<comment> \<open>fragile rule application!\<close>
     show "P 0" sorry
   next
     fix n :: nat
@@ -503,7 +503,7 @@
     from \<open>A x 0\<close> show "Q x 0" sorry
   next
     case (Suc n)
-    from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  -- \<open>arbitrary instances can be produced here\<close>
+    from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  \<comment> \<open>arbitrary instances can be produced here\<close>
       and \<open>A x (Suc n)\<close> show "Q x (Suc n)" sorry
   qed
 end
@@ -675,9 +675,9 @@
 begin
   assume a: A and b: B
   thm conjI
-  thm conjI [of A B]  -- "instantiation"
-  thm conjI [of A B, OF a b]  -- "instantiation and composition"
-  thm conjI [OF a b]  -- "composition via unification (trivial)"
+  thm conjI [of A B]  \<comment> "instantiation"
+  thm conjI [of A B, OF a b]  \<comment> "instantiation and composition"
+  thm conjI [OF a b]  \<comment> "composition via unification (trivial)"
   thm conjI [OF \<open>A\<close> \<open>B\<close>]
 
   thm conjI [OF disjI1]
@@ -710,9 +710,9 @@
       fix x
       assume "A x"
       show "B x" sorry
-    } -- "implicit block structure made explicit"
+    } \<comment> "implicit block structure made explicit"
     note \<open>\<And>x. A x \<Longrightarrow> B x\<close>
-      -- "side exit for the resulting rule"
+      \<comment> "side exit for the resulting rule"
   qed
 end
 
@@ -726,12 +726,12 @@
 
 notepad
 begin
-  assume r1: "A \<Longrightarrow> B \<Longrightarrow> C"  -- \<open>simple rule (Horn clause)\<close>
+  assume r1: "A \<Longrightarrow> B \<Longrightarrow> C"  \<comment> \<open>simple rule (Horn clause)\<close>
 
-  have A sorry  -- "prefix of facts via outer sub-proof"
+  have A sorry  \<comment> "prefix of facts via outer sub-proof"
   then have C
   proof (rule r1)
-    show B sorry  -- "remaining rule premises via inner sub-proof"
+    show B sorry  \<comment> "remaining rule premises via inner sub-proof"
   qed
 
   have C
@@ -750,7 +750,7 @@
 
 next
 
-  assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C"  -- \<open>nested rule\<close>
+  assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C"  \<comment> \<open>nested rule\<close>
 
   have A sorry
   then have C
@@ -850,31 +850,31 @@
 notepad
 begin
   have "A \<and> B"
-  proof  -- \<open>two strictly isolated subproofs\<close>
+  proof  \<comment> \<open>two strictly isolated subproofs\<close>
     show A sorry
   next
     show B sorry
   qed
 
   have "A \<and> B"
-  proof  -- \<open>one simultaneous sub-proof\<close>
+  proof  \<comment> \<open>one simultaneous sub-proof\<close>
     show A and B sorry
   qed
 
   have "A \<and> B"
-  proof  -- \<open>two subproofs in the same context\<close>
+  proof  \<comment> \<open>two subproofs in the same context\<close>
     show A sorry
     show B sorry
   qed
 
   have "A \<and> B"
-  proof  -- \<open>swapped order\<close>
+  proof  \<comment> \<open>swapped order\<close>
     show B sorry
     show A sorry
   qed
 
   have "A \<and> B"
-  proof  -- \<open>sequential subproofs\<close>
+  proof  \<comment> \<open>sequential subproofs\<close>
     show A sorry
     show B using \<open>A\<close> sorry
   qed
@@ -941,9 +941,9 @@
   following typical representatives:
 \<close>
 
-thm exE     -- \<open>local parameter\<close>
-thm conjE   -- \<open>local premises\<close>
-thm disjE   -- \<open>split into cases\<close>
+thm exE     \<comment> \<open>local parameter\<close>
+thm conjE   \<comment> \<open>local premises\<close>
+thm disjE   \<comment> \<open>split into cases\<close>
 
 text \<open>
   Combining these characteristics leads to the following general scheme
@@ -1001,7 +1001,7 @@
 print_statement disjE
 
 lemma
-  assumes A1 and A2  -- \<open>assumptions\<close>
+  assumes A1 and A2  \<comment> \<open>assumptions\<close>
   obtains
     (case1)  x y where "B1 x y" and "C1 x y"
   | (case2)  x y where "B2 x y" and "C2 x y"