isabelle update_cartouches -c;
authorwenzelm
Thu Nov 05 00:17:13 2015 +0100 (2015-11-05)
changeset 61580c49a8ebd30cc
parent 61579 634cd44bb1d3
child 61582 69492d32263a
isabelle update_cartouches -c;
src/Doc/Eisbach/Manual.thy
src/Doc/Implementation/ML.thy
src/Doc/Implementation/Prelim.thy
src/Doc/Implementation/Proof.thy
src/Doc/Isar_Ref/First_Order_Logic.thy
src/Doc/Isar_Ref/Synopsis.thy
     1.1 --- a/src/Doc/Eisbach/Manual.thy	Thu Nov 05 00:02:30 2015 +0100
     1.2 +++ b/src/Doc/Eisbach/Manual.thy	Thu Nov 05 00:17:13 2015 +0100
     1.3 @@ -249,16 +249,16 @@
     1.4  \<close>
     1.5  
     1.6      lemmas [intros] =
     1.7 -      conjI  --  \<open>@{thm conjI}\<close>
     1.8 -      impI  --  \<open>@{thm impI}\<close>
     1.9 -      disjCI  --  \<open>@{thm disjCI}\<close>
    1.10 -      iffI  --  \<open>@{thm iffI}\<close>
    1.11 -      notI  --  \<open>@{thm notI}\<close>
    1.12 +      conjI  \<comment>  \<open>@{thm conjI}\<close>
    1.13 +      impI  \<comment>  \<open>@{thm impI}\<close>
    1.14 +      disjCI  \<comment>  \<open>@{thm disjCI}\<close>
    1.15 +      iffI  \<comment>  \<open>@{thm iffI}\<close>
    1.16 +      notI  \<comment>  \<open>@{thm notI}\<close>
    1.17  
    1.18      lemmas [elims] =
    1.19 -      impCE  --  \<open>@{thm impCE}\<close>
    1.20 -      conjE  --  \<open>@{thm conjE}\<close>
    1.21 -      disjE  --  \<open>@{thm disjE}\<close>
    1.22 +      impCE  \<comment>  \<open>@{thm impCE}\<close>
    1.23 +      conjE  \<comment>  \<open>@{thm conjE}\<close>
    1.24 +      disjE  \<comment>  \<open>@{thm disjE}\<close>
    1.25  
    1.26      lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
    1.27        by prop_solver
     2.1 --- a/src/Doc/Implementation/ML.thy	Thu Nov 05 00:02:30 2015 +0100
     2.2 +++ b/src/Doc/Implementation/ML.thy	Thu Nov 05 00:17:13 2015 +0100
     2.3 @@ -578,7 +578,7 @@
     2.4    ML_prf %"ML" \<open>val a = 1\<close>
     2.5    {
     2.6      ML_prf %"ML" \<open>val b = a + 1\<close>
     2.7 -  } -- \<open>Isar block structure ignored by ML environment\<close>
     2.8 +  } \<comment> \<open>Isar block structure ignored by ML environment\<close>
     2.9    ML_prf %"ML" \<open>val c = b + 1\<close>
    2.10  end
    2.11  
     3.1 --- a/src/Doc/Implementation/Prelim.thy	Thu Nov 05 00:02:30 2015 +0100
     3.2 +++ b/src/Doc/Implementation/Prelim.thy	Thu Nov 05 00:17:13 2015 +0100
     3.3 @@ -471,17 +471,17 @@
     3.4  begin
     3.5  
     3.6  declare [[show_types = false]]
     3.7 -  -- \<open>declaration within (local) theory context\<close>
     3.8 +  \<comment> \<open>declaration within (local) theory context\<close>
     3.9  
    3.10  notepad
    3.11  begin
    3.12    note [[show_types = true]]
    3.13 -    -- \<open>declaration within proof (forward mode)\<close>
    3.14 +    \<comment> \<open>declaration within proof (forward mode)\<close>
    3.15    term x
    3.16  
    3.17    have "x = x"
    3.18      using [[show_types = false]]
    3.19 -      -- \<open>declaration within proof (backward mode)\<close>
    3.20 +      \<comment> \<open>declaration within proof (backward mode)\<close>
    3.21      ..
    3.22  end
    3.23  
     4.1 --- a/src/Doc/Implementation/Proof.thy	Thu Nov 05 00:02:30 2015 +0100
     4.2 +++ b/src/Doc/Implementation/Proof.thy	Thu Nov 05 00:17:13 2015 +0100
     4.3 @@ -58,14 +58,14 @@
     4.4  notepad
     4.5  begin
     4.6    {
     4.7 -    fix x  -- \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
     4.8 +    fix x  \<comment> \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
     4.9      {
    4.10 -      have "x::'a \<equiv> x"  -- \<open>implicit type assignment by concrete occurrence\<close>
    4.11 +      have "x::'a \<equiv> x"  \<comment> \<open>implicit type assignment by concrete occurrence\<close>
    4.12          by (rule reflexive)
    4.13      }
    4.14 -    thm this  -- \<open>result still with fixed type \<open>'a\<close>\<close>
    4.15 +    thm this  \<comment> \<open>result still with fixed type \<open>'a\<close>\<close>
    4.16    }
    4.17 -  thm this  -- \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
    4.18 +  thm this  \<comment> \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
    4.19  end
    4.20  
    4.21  text \<open>The Isabelle/Isar proof context manages the details of term
     5.1 --- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 05 00:02:30 2015 +0100
     5.2 +++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 05 00:17:13 2015 +0100
     5.3 @@ -357,10 +357,10 @@
     5.4  theorem
     5.5    assumes "\<exists>x. \<forall>y. R x y"
     5.6    shows "\<forall>y. \<exists>x. R x y"
     5.7 -proof    -- \<open>\<open>\<forall>\<close> introduction\<close>
     5.8 -  obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> ..    -- \<open>\<open>\<exists>\<close> elimination\<close>
     5.9 -  fix y have "R x y" using \<open>\<forall>y. R x y\<close> ..    -- \<open>\<open>\<forall>\<close> destruction\<close>
    5.10 -  then show "\<exists>x. R x y" ..    -- \<open>\<open>\<exists>\<close> introduction\<close>
    5.11 +proof    \<comment> \<open>\<open>\<forall>\<close> introduction\<close>
    5.12 +  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>
    5.13 +  fix y have "R x y" using \<open>\<forall>y. R x y\<close> ..    \<comment> \<open>\<open>\<forall>\<close> destruction\<close>
    5.14 +  then show "\<exists>x. R x y" ..    \<comment> \<open>\<open>\<exists>\<close> introduction\<close>
    5.15  qed
    5.16  
    5.17  
     6.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Thu Nov 05 00:02:30 2015 +0100
     6.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Thu Nov 05 00:17:13 2015 +0100
     6.3 @@ -17,11 +17,11 @@
     6.4  notepad
     6.5  begin
     6.6    txt \<open>Locally fixed entities:\<close>
     6.7 -  fix x   -- \<open>local constant, without any type information yet\<close>
     6.8 -  fix x :: 'a  -- \<open>variant with explicit type-constraint for subsequent use\<close>
     6.9 +  fix x   \<comment> \<open>local constant, without any type information yet\<close>
    6.10 +  fix x :: 'a  \<comment> \<open>variant with explicit type-constraint for subsequent use\<close>
    6.11  
    6.12    fix a b
    6.13 -  assume "a = b"  -- \<open>type assignment at first occurrence in concrete term\<close>
    6.14 +  assume "a = b"  \<comment> \<open>type assignment at first occurrence in concrete term\<close>
    6.15  
    6.16    txt \<open>Definitions (non-polymorphic):\<close>
    6.17    def x \<equiv> "t::'a"
    6.18 @@ -234,7 +234,7 @@
    6.19    proof -
    6.20      term ?thesis
    6.21      show ?thesis sorry
    6.22 -    term ?thesis  -- \<open>static!\<close>
    6.23 +    term ?thesis  \<comment> \<open>static!\<close>
    6.24    qed
    6.25    term "\<dots>"
    6.26    thm this
    6.27 @@ -345,7 +345,7 @@
    6.28    moreover
    6.29    { assume C have R sorry }
    6.30    ultimately
    6.31 -  have R by blast  -- \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
    6.32 +  have R by blast  \<comment> \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
    6.33  end
    6.34  
    6.35  
    6.36 @@ -364,7 +364,7 @@
    6.37  begin
    6.38    fix n :: nat
    6.39    have "P n"
    6.40 -  proof (rule nat.induct)  -- \<open>fragile rule application!\<close>
    6.41 +  proof (rule nat.induct)  \<comment> \<open>fragile rule application!\<close>
    6.42      show "P 0" sorry
    6.43    next
    6.44      fix n :: nat
    6.45 @@ -503,7 +503,7 @@
    6.46      from \<open>A x 0\<close> show "Q x 0" sorry
    6.47    next
    6.48      case (Suc n)
    6.49 -    from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  -- \<open>arbitrary instances can be produced here\<close>
    6.50 +    from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  \<comment> \<open>arbitrary instances can be produced here\<close>
    6.51        and \<open>A x (Suc n)\<close> show "Q x (Suc n)" sorry
    6.52    qed
    6.53  end
    6.54 @@ -675,9 +675,9 @@
    6.55  begin
    6.56    assume a: A and b: B
    6.57    thm conjI
    6.58 -  thm conjI [of A B]  -- "instantiation"
    6.59 -  thm conjI [of A B, OF a b]  -- "instantiation and composition"
    6.60 -  thm conjI [OF a b]  -- "composition via unification (trivial)"
    6.61 +  thm conjI [of A B]  \<comment> "instantiation"
    6.62 +  thm conjI [of A B, OF a b]  \<comment> "instantiation and composition"
    6.63 +  thm conjI [OF a b]  \<comment> "composition via unification (trivial)"
    6.64    thm conjI [OF \<open>A\<close> \<open>B\<close>]
    6.65  
    6.66    thm conjI [OF disjI1]
    6.67 @@ -710,9 +710,9 @@
    6.68        fix x
    6.69        assume "A x"
    6.70        show "B x" sorry
    6.71 -    } -- "implicit block structure made explicit"
    6.72 +    } \<comment> "implicit block structure made explicit"
    6.73      note \<open>\<And>x. A x \<Longrightarrow> B x\<close>
    6.74 -      -- "side exit for the resulting rule"
    6.75 +      \<comment> "side exit for the resulting rule"
    6.76    qed
    6.77  end
    6.78  
    6.79 @@ -726,12 +726,12 @@
    6.80  
    6.81  notepad
    6.82  begin
    6.83 -  assume r1: "A \<Longrightarrow> B \<Longrightarrow> C"  -- \<open>simple rule (Horn clause)\<close>
    6.84 +  assume r1: "A \<Longrightarrow> B \<Longrightarrow> C"  \<comment> \<open>simple rule (Horn clause)\<close>
    6.85  
    6.86 -  have A sorry  -- "prefix of facts via outer sub-proof"
    6.87 +  have A sorry  \<comment> "prefix of facts via outer sub-proof"
    6.88    then have C
    6.89    proof (rule r1)
    6.90 -    show B sorry  -- "remaining rule premises via inner sub-proof"
    6.91 +    show B sorry  \<comment> "remaining rule premises via inner sub-proof"
    6.92    qed
    6.93  
    6.94    have C
    6.95 @@ -750,7 +750,7 @@
    6.96  
    6.97  next
    6.98  
    6.99 -  assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C"  -- \<open>nested rule\<close>
   6.100 +  assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C"  \<comment> \<open>nested rule\<close>
   6.101  
   6.102    have A sorry
   6.103    then have C
   6.104 @@ -850,31 +850,31 @@
   6.105  notepad
   6.106  begin
   6.107    have "A \<and> B"
   6.108 -  proof  -- \<open>two strictly isolated subproofs\<close>
   6.109 +  proof  \<comment> \<open>two strictly isolated subproofs\<close>
   6.110      show A sorry
   6.111    next
   6.112      show B sorry
   6.113    qed
   6.114  
   6.115    have "A \<and> B"
   6.116 -  proof  -- \<open>one simultaneous sub-proof\<close>
   6.117 +  proof  \<comment> \<open>one simultaneous sub-proof\<close>
   6.118      show A and B sorry
   6.119    qed
   6.120  
   6.121    have "A \<and> B"
   6.122 -  proof  -- \<open>two subproofs in the same context\<close>
   6.123 +  proof  \<comment> \<open>two subproofs in the same context\<close>
   6.124      show A sorry
   6.125      show B sorry
   6.126    qed
   6.127  
   6.128    have "A \<and> B"
   6.129 -  proof  -- \<open>swapped order\<close>
   6.130 +  proof  \<comment> \<open>swapped order\<close>
   6.131      show B sorry
   6.132      show A sorry
   6.133    qed
   6.134  
   6.135    have "A \<and> B"
   6.136 -  proof  -- \<open>sequential subproofs\<close>
   6.137 +  proof  \<comment> \<open>sequential subproofs\<close>
   6.138      show A sorry
   6.139      show B using \<open>A\<close> sorry
   6.140    qed
   6.141 @@ -941,9 +941,9 @@
   6.142    following typical representatives:
   6.143  \<close>
   6.144  
   6.145 -thm exE     -- \<open>local parameter\<close>
   6.146 -thm conjE   -- \<open>local premises\<close>
   6.147 -thm disjE   -- \<open>split into cases\<close>
   6.148 +thm exE     \<comment> \<open>local parameter\<close>
   6.149 +thm conjE   \<comment> \<open>local premises\<close>
   6.150 +thm disjE   \<comment> \<open>split into cases\<close>
   6.151  
   6.152  text \<open>
   6.153    Combining these characteristics leads to the following general scheme
   6.154 @@ -1001,7 +1001,7 @@
   6.155  print_statement disjE
   6.156  
   6.157  lemma
   6.158 -  assumes A1 and A2  -- \<open>assumptions\<close>
   6.159 +  assumes A1 and A2  \<comment> \<open>assumptions\<close>
   6.160    obtains
   6.161      (case1)  x y where "B1 x y" and "C1 x y"
   6.162    | (case2)  x y where "B2 x y" and "C2 x y"