replaced ?? by ?;
authorwenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 74800a0e0dbe1269
parent 7479 b482d827899c
child 7481 d44c77be268c
replaced ?? by ?;
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/Cantor.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/Group.thy
src/HOL/Isar_examples/KnasterTarski.thy
src/HOL/Isar_examples/MultisetOrder.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/Summation.thy
src/HOL/ex/Points.thy
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 04 21:12:15 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 04 21:13:01 1999 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4    then; show "B & A";
     1.5    proof;
     1.6      assume A B;
     1.7 -    show ??thesis; ..;
     1.8 +    show ?thesis; ..;
     1.9    qed;
    1.10  qed;
    1.11  
    1.12 @@ -123,8 +123,8 @@
    1.13    then; show "EX x. P(x)";
    1.14    proof (rule exE);
    1.15      fix a;
    1.16 -    assume "P(f(a))" (is "P(??witness)");
    1.17 -    show ??thesis; by (rule exI [of P ??witness]);
    1.18 +    assume "P(f(a))" (is "P(?witness)");
    1.19 +    show ?thesis; by (rule exI [of P ?witness]);
    1.20    qed;
    1.21  qed;
    1.22  
    1.23 @@ -135,7 +135,7 @@
    1.24    proof;
    1.25      fix a;
    1.26      assume "P(f(a))";
    1.27 -    show ??thesis; ..;
    1.28 +    show ?thesis; ..;
    1.29    qed;
    1.30  qed;
    1.31  
     2.1 --- a/src/HOL/Isar_examples/Cantor.thy	Sat Sep 04 21:12:15 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Sat Sep 04 21:13:01 1999 +0200
     2.3 @@ -34,25 +34,25 @@
     2.4  
     2.5  theorem "EX S. S ~: range(f :: 'a => 'a set)";
     2.6  proof;
     2.7 -  let ??S = "{x. x ~: f x}";
     2.8 -  show "??S ~: range f";
     2.9 +  let ?S = "{x. x ~: f x}";
    2.10 +  show "?S ~: range f";
    2.11    proof;
    2.12 -    assume "??S : range f";
    2.13 +    assume "?S : range f";
    2.14      then; show False;
    2.15      proof;
    2.16        fix y; 
    2.17 -      assume "??S = f y";
    2.18 -      then; show ??thesis;
    2.19 +      assume "?S = f y";
    2.20 +      then; show ?thesis;
    2.21        proof (rule equalityCE);
    2.22 -        assume y_in_S: "y : ??S";
    2.23 +        assume y_in_S: "y : ?S";
    2.24          assume y_in_fy: "y : f y";
    2.25          from y_in_S; have y_notin_fy: "y ~: f y"; ..;
    2.26 -        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
    2.27 +        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
    2.28        next;
    2.29 -        assume y_notin_S: "y ~: ??S";
    2.30 +        assume y_notin_S: "y ~: ?S";
    2.31          assume y_notin_fy: "y ~: f y";
    2.32          from y_notin_S; have y_in_fy: "y : f y"; ..;
    2.33 -        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
    2.34 +        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
    2.35        qed;
    2.36      qed;
    2.37    qed;
    2.38 @@ -67,23 +67,23 @@
    2.39  
    2.40  theorem "EX S. S ~: range(f :: 'a => 'a set)";
    2.41  proof;
    2.42 -  let ??S = "{x. x ~: f x}";
    2.43 -  show "??S ~: range f";
    2.44 +  let ?S = "{x. x ~: f x}";
    2.45 +  show "?S ~: range f";
    2.46    proof;
    2.47 -    assume "??S : range f";
    2.48 +    assume "?S : range f";
    2.49      thus False;
    2.50      proof;
    2.51        fix y; 
    2.52 -      assume "??S = f y";
    2.53 -      thus ??thesis;
    2.54 +      assume "?S = f y";
    2.55 +      thus ?thesis;
    2.56        proof (rule equalityCE);
    2.57          assume "y : f y";
    2.58 -        assume "y : ??S"; hence "y ~: f y"; ..;
    2.59 -        thus ??thesis; by contradiction;
    2.60 +        assume "y : ?S"; hence "y ~: f y"; ..;
    2.61 +        thus ?thesis; by contradiction;
    2.62        next;
    2.63          assume "y ~: f y";
    2.64 -        assume "y ~: ??S"; hence "y : f y"; ..;
    2.65 -        thus ??thesis; by contradiction;
    2.66 +        assume "y ~: ?S"; hence "y : f y"; ..;
    2.67 +        thus ?thesis; by contradiction;
    2.68        qed;
    2.69      qed;
    2.70    qed;
     3.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Sat Sep 04 21:12:15 1999 +0200
     3.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sat Sep 04 21:13:01 1999 +0200
     3.3 @@ -100,30 +100,30 @@
     3.4  *};
     3.5  
     3.6  lemma exec_append:
     3.7 -  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
     3.8 -proof (induct ??P xs type: list);
     3.9 -  show "??P []"; by simp;
    3.10 +  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs");
    3.11 +proof (induct ?P xs type: list);
    3.12 +  show "?P []"; by simp;
    3.13  
    3.14    fix x xs;
    3.15 -  assume "??P xs";
    3.16 -  show "??P (x # xs)" (is "??Q x");
    3.17 -  proof (induct ??Q x type: instr);
    3.18 -    fix val; show "??Q (Const val)"; by force;
    3.19 +  assume "?P xs";
    3.20 +  show "?P (x # xs)" (is "?Q x");
    3.21 +  proof (induct ?Q x type: instr);
    3.22 +    fix val; show "?Q (Const val)"; by force;
    3.23    next;
    3.24 -    fix adr; show "??Q (Load adr)"; by force;
    3.25 +    fix adr; show "?Q (Load adr)"; by force;
    3.26    next;
    3.27 -    fix fun; show "??Q (Apply fun)"; by force;
    3.28 +    fix fun; show "?Q (Apply fun)"; by force;
    3.29    qed;
    3.30  qed;
    3.31  
    3.32  lemma exec_comp:
    3.33 -  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
    3.34 -proof (induct ??P e type: expr);
    3.35 -  fix adr; show "??P (Variable adr)"; by force;
    3.36 +  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
    3.37 +proof (induct ?P e type: expr);
    3.38 +  fix adr; show "?P (Variable adr)"; by force;
    3.39  next;
    3.40 -  fix val; show "??P (Constant val)"; by force;
    3.41 +  fix val; show "?P (Constant val)"; by force;
    3.42  next;
    3.43 -  fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
    3.44 +  fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
    3.45      by (force simp add: exec_append);
    3.46  qed;
    3.47  
     4.1 --- a/src/HOL/Isar_examples/Group.thy	Sat Sep 04 21:12:15 1999 +0200
     4.2 +++ b/src/HOL/Isar_examples/Group.thy	Sat Sep 04 21:13:01 1999 +0200
     4.3 @@ -49,7 +49,7 @@
     4.4      by (simp only: group_left_unit);
     4.5    also; have "... = one";
     4.6      by (simp only: group_left_inverse);
     4.7 -  finally; show ??thesis; .;
     4.8 +  finally; show ?thesis; .;
     4.9  qed;
    4.10  
    4.11  text {*
    4.12 @@ -67,7 +67,7 @@
    4.13      by (simp only: group_right_inverse);
    4.14    also; have "... = x";
    4.15      by (simp only: group_left_unit);
    4.16 -  finally; show ??thesis; .;
    4.17 +  finally; show ?thesis; .;
    4.18  qed;
    4.19  
    4.20  text {*
    4.21 @@ -80,7 +80,7 @@
    4.22  
    4.23   Note that "..." is just a special term binding that happens to be
    4.24   bound automatically to the argument of the last fact established by
    4.25 - assume or any local goal.  In contrast to ??thesis, "..." is bound
    4.26 + assume or any local goal.  In contrast to ?thesis, "..." is bound
    4.27   after the proof is finished.
    4.28  *};
    4.29  
    4.30 @@ -112,7 +112,7 @@
    4.31    from calculation
    4.32      -- {* ... and pick up final result *};
    4.33  
    4.34 -  show ??thesis; .;
    4.35 +  show ?thesis; .;
    4.36  qed;
    4.37  
    4.38  
     5.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Sat Sep 04 21:12:15 1999 +0200
     5.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sat Sep 04 21:13:01 1999 +0200
     5.3 @@ -37,28 +37,28 @@
     5.4  
     5.5  theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
     5.6  proof;
     5.7 -  let ??H = "{u. f u <= u}";
     5.8 -  let ??a = "Inter ??H";
     5.9 +  let ?H = "{u. f u <= u}";
    5.10 +  let ?a = "Inter ?H";
    5.11  
    5.12    assume mono: "mono f";
    5.13 -  show "f ??a = ??a";
    5.14 +  show "f ?a = ?a";
    5.15    proof -;
    5.16      {{;
    5.17        fix x;
    5.18 -      assume mem: "x : ??H";
    5.19 -      hence "??a <= x"; by (rule Inter_lower);
    5.20 -      with mono; have "f ??a <= f x"; ..;
    5.21 +      assume mem: "x : ?H";
    5.22 +      hence "?a <= x"; by (rule Inter_lower);
    5.23 +      with mono; have "f ?a <= f x"; ..;
    5.24        also; from mem; have "... <= x"; ..;
    5.25 -      finally; have "f ??a <= x"; .;
    5.26 +      finally; have "f ?a <= x"; .;
    5.27      }};
    5.28 -    hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
    5.29 +    hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
    5.30      {{;
    5.31 -      also; presume "... <= f ??a";
    5.32 -      finally (order_antisym); show ??thesis; .;
    5.33 +      also; presume "... <= f ?a";
    5.34 +      finally (order_antisym); show ?thesis; .;
    5.35      }};
    5.36 -    from mono ge; have "f (f ??a) <= f ??a"; ..;
    5.37 -    hence "f ??a : ??H"; ..;
    5.38 -    thus "??a <= f ??a"; by (rule Inter_lower);
    5.39 +    from mono ge; have "f (f ?a) <= f ?a"; ..;
    5.40 +    hence "f ?a : ?H"; ..;
    5.41 +    thus "?a <= f ?a"; by (rule Inter_lower);
    5.42    qed;
    5.43  qed;
    5.44  
     6.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Sat Sep 04 21:12:15 1999 +0200
     6.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sat Sep 04 21:13:01 1999 +0200
     6.3 @@ -14,50 +14,50 @@
     6.4  
     6.5  lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
     6.6  proof;
     6.7 -  let ??R = "mult1 r";
     6.8 -  let ??W = "acc ??R";
     6.9 +  let ?R = "mult1 r";
    6.10 +  let ?W = "acc ?R";
    6.11  
    6.12  
    6.13    {{;
    6.14      fix M M0 a;
    6.15 -    assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)"
    6.16 -      and M0: "M0 : ??W"
    6.17 -      and acc_hyp: "ALL M. (M, M0) : ??R --> M + {#a#} : ??W";
    6.18 -    have "M0 + {#a#} : ??W";
    6.19 +    assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
    6.20 +      and M0: "M0 : ?W"
    6.21 +      and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
    6.22 +    have "M0 + {#a#} : ?W";
    6.23      proof (rule accI [of "M0 + {#a#}"]);
    6.24 -      fix N; assume "(N, M0 + {#a#}) : ??R";
    6.25 -      hence "((EX M. (M, M0) : ??R & N = M + {#a#}) |
    6.26 +      fix N; assume "(N, M0 + {#a#}) : ?R";
    6.27 +      hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
    6.28               (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
    6.29  	by (simp only: less_add_conv);
    6.30 -      thus "N : ??W";
    6.31 +      thus "N : ?W";
    6.32        proof (elim exE disjE conjE);
    6.33 -	fix M; assume "(M, M0) : ??R" and N: "N = M + {#a#}";
    6.34 -	from acc_hyp; have "(M, M0) : ??R --> M + {#a#} : ??W"; ..;
    6.35 -	hence "M + {#a#} : ??W"; ..;
    6.36 -	thus "N : ??W"; by (simp only: N);
    6.37 +	fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}";
    6.38 +	from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..;
    6.39 +	hence "M + {#a#} : ?W"; ..;
    6.40 +	thus "N : ?W"; by (simp only: N);
    6.41        next;
    6.42  	fix K;
    6.43  	assume N: "N = M0 + K";
    6.44  	assume "ALL b. elem K b --> (b, a) : r";
    6.45 -	have "??this --> M0 + K : ??W" (is "??P K");
    6.46 +	have "?this --> M0 + K : ?W" (is "?P K");
    6.47  	proof (rule multiset_induct [of _ K]);
    6.48 -	  from M0; have "M0 + {#} : ??W"; by simp;
    6.49 -	  thus "??P {#}"; ..;
    6.50 +	  from M0; have "M0 + {#} : ?W"; by simp;
    6.51 +	  thus "?P {#}"; ..;
    6.52  
    6.53 -	  fix K x; assume hyp: "??P K";
    6.54 -	  show "??P (K + {#x#})";
    6.55 +	  fix K x; assume hyp: "?P K";
    6.56 +	  show "?P (K + {#x#})";
    6.57  	  proof;
    6.58  	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
    6.59  	    hence "(x, a) : r"; by simp;
    6.60 -	    with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..;
    6.61 +	    with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..;
    6.62  
    6.63 -	    from a hyp; have "M0 + K : ??W"; by simp;
    6.64 -	    with b; have "(M0 + K) + {#x#} : ??W"; ..;
    6.65 -	    thus "M0 + (K + {#x#}) : ??W"; by (simp only: union_assoc);
    6.66 +	    from a hyp; have "M0 + K : ?W"; by simp;
    6.67 +	    with b; have "(M0 + K) + {#x#} : ?W"; ..;
    6.68 +	    thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc);
    6.69  	  qed;
    6.70  	qed;
    6.71 -	hence "M0 + K : ??W"; ..;
    6.72 -	thus "N : ??W"; by (simp only: N);
    6.73 +	hence "M0 + K : ?W"; ..;
    6.74 +	thus "N : ?W"; by (simp only: N);
    6.75        qed;
    6.76      qed;
    6.77    }}; note tedious_reasoning = this;
    6.78 @@ -65,25 +65,25 @@
    6.79  
    6.80    assume wf: "wf r";
    6.81    fix M;
    6.82 -  show "M : ??W";
    6.83 +  show "M : ?W";
    6.84    proof (rule multiset_induct [of _ M]);
    6.85 -    show "{#} : ??W";
    6.86 +    show "{#} : ?W";
    6.87      proof (rule accI);
    6.88 -      fix b; assume "(b, {#}) : ??R";
    6.89 -      with not_less_empty; show "b : ??W"; by contradiction;
    6.90 +      fix b; assume "(b, {#}) : ?R";
    6.91 +      with not_less_empty; show "b : ?W"; by contradiction;
    6.92      qed;
    6.93  
    6.94 -    fix M a; assume "M : ??W";
    6.95 -    from wf; have "ALL M:??W. M + {#a#} : ??W";
    6.96 +    fix M a; assume "M : ?W";
    6.97 +    from wf; have "ALL M:?W. M + {#a#} : ?W";
    6.98      proof (rule wf_induct [of r]);
    6.99 -      fix a; assume "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)";
   6.100 -      show "ALL M:??W. M + {#a#} : ??W";
   6.101 +      fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
   6.102 +      show "ALL M:?W. M + {#a#} : ?W";
   6.103        proof;
   6.104 -	fix M; assume "M : ??W";
   6.105 -	thus "M + {#a#} : ??W"; by (rule acc_induct) (rule tedious_reasoning);
   6.106 +	fix M; assume "M : ?W";
   6.107 +	thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning);
   6.108        qed;
   6.109      qed;
   6.110 -    thus "M + {#a#} : ??W"; ..;
   6.111 +    thus "M + {#a#} : ?W"; ..;
   6.112    qed;
   6.113  qed;
   6.114  
     7.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Sep 04 21:12:15 1999 +0200
     7.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Sep 04 21:13:01 1999 +0200
     7.3 @@ -28,21 +28,21 @@
     7.4  
     7.5  lemma tiling_Un: "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
     7.6  proof;
     7.7 -  assume "t : tiling A" (is "_ : ??T");
     7.8 -  thus "u : ??T --> t Int u = {} --> t Un u : ??T" (is "??P t");
     7.9 +  assume "t : tiling A" (is "_ : ?T");
    7.10 +  thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
    7.11    proof (induct t set: tiling);
    7.12 -    show "??P {}"; by simp;
    7.13 +    show "?P {}"; by simp;
    7.14  
    7.15      fix a t;
    7.16 -    assume "a : A" "t : ??T" "??P t" "a <= - t";
    7.17 -    show "??P (a Un t)";
    7.18 +    assume "a : A" "t : ?T" "?P t" "a <= - t";
    7.19 +    show "?P (a Un t)";
    7.20      proof (intro impI);
    7.21 -      assume "u : ??T" "(a Un t) Int u = {}";
    7.22 -      have hyp: "t Un u: ??T"; by blast;
    7.23 +      assume "u : ?T" "(a Un t) Int u = {}";
    7.24 +      have hyp: "t Un u: ?T"; by blast;
    7.25        have "a <= - (t Un u)"; by blast;
    7.26 -      with _ hyp; have "a Un (t Un u) : ??T"; by (rule tiling.Un);
    7.27 +      with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
    7.28        also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
    7.29 -      finally; show "... : ??T"; .;
    7.30 +      finally; show "... : ?T"; .;
    7.31      qed;
    7.32    qed;
    7.33  qed;
    7.34 @@ -113,41 +113,41 @@
    7.35  
    7.36  
    7.37  lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
    7.38 -  (is "??P n" is "??B n : ??T");
    7.39 +  (is "?P n" is "?B n : ?T");
    7.40  proof (induct n);
    7.41 -  show "??P 0"; by (simp add: below_0 tiling.empty);
    7.42 +  show "?P 0"; by (simp add: below_0 tiling.empty);
    7.43  
    7.44 -  fix n; assume hyp: "??P n";
    7.45 -  let ??a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
    7.46 +  fix n; assume hyp: "?P n";
    7.47 +  let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
    7.48  
    7.49 -  have "??B (Suc n) = ??a Un ??B n"; by (simp add: Sigma_Suc Un_assoc);
    7.50 -  also; have "... : ??T";
    7.51 +  have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
    7.52 +  also; have "... : ?T";
    7.53    proof (rule tiling.Un);
    7.54      have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz);
    7.55 -    also; have "{(i, 2 * n), (i, 2 * n + 1)} = ??a"; by blast;
    7.56 +    also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast;
    7.57      finally; show "... : domino"; .;
    7.58 -    from hyp; show "??B n : ??T"; .;
    7.59 -    show "??a <= - ??B n"; by force;
    7.60 +    from hyp; show "?B n : ?T"; .;
    7.61 +    show "?a <= - ?B n"; by force;
    7.62    qed;
    7.63 -  finally; show "??P (Suc n)"; .;
    7.64 +  finally; show "?P (Suc n)"; .;
    7.65  qed;
    7.66  
    7.67  lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino"
    7.68 -  (is "??P m" is "??B m : ??T");
    7.69 +  (is "?P m" is "?B m : ?T");
    7.70  proof (induct m);
    7.71 -  show "??P 0"; by (simp add: below_0 tiling.empty);
    7.72 +  show "?P 0"; by (simp add: below_0 tiling.empty);
    7.73  
    7.74 -  fix m; assume hyp: "??P m";
    7.75 -  let ??t = "{m} Times below (2 * n)";
    7.76 +  fix m; assume hyp: "?P m";
    7.77 +  let ?t = "{m} Times below (2 * n)";
    7.78  
    7.79 -  have "??B (Suc m) = ??t Un ??B m"; by (simp add: Sigma_Suc);
    7.80 -  also; have "... : ??T";
    7.81 +  have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
    7.82 +  also; have "... : ?T";
    7.83    proof (rule tiling_Un [rulify]);
    7.84 -    show "??t : ??T"; by (rule dominoes_tile_row);
    7.85 -    from hyp; show "??B m : ??T"; .;
    7.86 -    show "??t Int ??B m = {}"; by blast;
    7.87 +    show "?t : ?T"; by (rule dominoes_tile_row);
    7.88 +    from hyp; show "?B m : ?T"; .;
    7.89 +    show "?t Int ?B m = {}"; by blast;
    7.90    qed;
    7.91 -  finally; show "??P (Suc m)"; .;
    7.92 +  finally; show "?P (Suc m)"; .;
    7.93  qed;
    7.94  
    7.95  
    7.96 @@ -155,13 +155,13 @@
    7.97  proof -;
    7.98    assume "b < 2";
    7.99    assume "d : domino";
   7.100 -  thus ??thesis (is "??P d");
   7.101 +  thus ?thesis (is "?P d");
   7.102    proof (induct d set: domino);
   7.103      have b_cases: "b = 0 | b = 1"; by arith;
   7.104      fix i j;
   7.105      note [simp] = evnodd_empty evnodd_insert mod_Suc;
   7.106 -    from b_cases; show "??P {(i, j), (i, j + 1)}"; by rule auto;
   7.107 -    from b_cases; show "??P {(i, j), (i + 1, j)}"; by rule auto;
   7.108 +    from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
   7.109 +    from b_cases; show "?P {(i, j), (i + 1, j)}"; by rule auto;
   7.110    qed;
   7.111  qed;
   7.112  
   7.113 @@ -175,54 +175,54 @@
   7.114  
   7.115  section {* Tilings of dominoes *};
   7.116  
   7.117 -lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ??T ==> ??F t");
   7.118 +lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
   7.119  proof -;
   7.120 -  assume "t : ??T";
   7.121 -  thus "??F t";
   7.122 +  assume "t : ?T";
   7.123 +  thus "?F t";
   7.124    proof (induct t set: tiling);
   7.125 -    show "??F {}"; by (rule Finites.emptyI);
   7.126 -    fix a t; assume "??F t";
   7.127 -    assume "a : domino"; hence "??F a"; by (rule domino_finite);
   7.128 -    thus "??F (a Un t)"; by (rule finite_UnI);
   7.129 +    show "?F {}"; by (rule Finites.emptyI);
   7.130 +    fix a t; assume "?F t";
   7.131 +    assume "a : domino"; hence "?F a"; by (rule domino_finite);
   7.132 +    thus "?F (a Un t)"; by (rule finite_UnI);
   7.133    qed;
   7.134  qed;
   7.135  
   7.136  lemma tiling_domino_01: "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
   7.137 -  (is "t : ??T ==> ??P t");
   7.138 +  (is "t : ?T ==> ?P t");
   7.139  proof -;
   7.140 -  assume "t : ??T";
   7.141 -  thus "??P t";
   7.142 +  assume "t : ?T";
   7.143 +  thus "?P t";
   7.144    proof (induct t set: tiling);
   7.145 -    show "??P {}"; by (simp add: evnodd_def);
   7.146 +    show "?P {}"; by (simp add: evnodd_def);
   7.147  
   7.148      fix a t;
   7.149 -    let ??e = evnodd;
   7.150 -    assume "a : domino" "t : ??T"
   7.151 -      and hyp: "card (??e t 0) = card (??e t 1)"
   7.152 +    let ?e = evnodd;
   7.153 +    assume "a : domino" "t : ?T"
   7.154 +      and hyp: "card (?e t 0) = card (?e t 1)"
   7.155        and "a <= - t";
   7.156  
   7.157 -    have card_suc: "!!b. b < 2 ==> card (??e (a Un t) b) = Suc (card (??e t b))";
   7.158 +    have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
   7.159      proof -;
   7.160        fix b; assume "b < 2";
   7.161 -      have "EX i j. ??e a b = {(i, j)}"; by (rule domino_singleton);
   7.162 -      thus "??thesis b";
   7.163 +      have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
   7.164 +      thus "?thesis b";
   7.165        proof (elim exE);
   7.166 -	have "??e (a Un t) b = ??e a b Un ??e t b"; by (rule evnodd_Un);
   7.167 -	also; fix i j; assume "??e a b = {(i, j)}";
   7.168 -	also; have "... Un ??e t b = insert (i, j) (??e t b)"; by simp;
   7.169 -	also; have "card ... = Suc (card (??e t b))";
   7.170 +	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
   7.171 +	also; fix i j; assume "?e a b = {(i, j)}";
   7.172 +	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
   7.173 +	also; have "card ... = Suc (card (?e t b))";
   7.174  	proof (rule card_insert_disjoint);
   7.175 -	  show "finite (??e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
   7.176 -	  have "(i, j) : ??e a b"; by asm_simp;
   7.177 -	  thus "(i, j) ~: ??e t b"; by (force dest: evnoddD);
   7.178 +	  show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
   7.179 +	  have "(i, j) : ?e a b"; by asm_simp;
   7.180 +	  thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
   7.181  	qed;
   7.182 -	finally; show ??thesis; .;
   7.183 +	finally; show ?thesis; .;
   7.184        qed;
   7.185      qed;
   7.186 -    hence "card (??e (a Un t) 0) = Suc (card (??e t 0))"; by simp;
   7.187 -    also; from hyp; have "card (??e t 0) = card (??e t 1)"; .;
   7.188 -    also; from card_suc; have "Suc ... = card (??e (a Un t) 1)"; by simp;
   7.189 -    finally; show "??P (a Un t)"; .;
   7.190 +    hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp;
   7.191 +    also; from hyp; have "card (?e t 0) = card (?e t 1)"; .;
   7.192 +    also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp;
   7.193 +    finally; show "?P (a Un t)"; .;
   7.194    qed;
   7.195  qed;
   7.196  
   7.197 @@ -236,37 +236,37 @@
   7.198  
   7.199  theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
   7.200  proof (unfold mutilated_board_def);
   7.201 -  let ??T = "tiling domino";
   7.202 -  let ??t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
   7.203 -  let ??t' = "??t - {(0, 0)}";
   7.204 -  let ??t'' = "??t' - {(2 * m + 1, 2 * n + 1)}";
   7.205 -  show "??t'' ~: ??T";
   7.206 +  let ?T = "tiling domino";
   7.207 +  let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
   7.208 +  let ?t' = "?t - {(0, 0)}";
   7.209 +  let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
   7.210 +  show "?t'' ~: ?T";
   7.211    proof;
   7.212 -    have t: "??t : ??T"; by (rule dominoes_tile_matrix);
   7.213 -    assume t'': "??t'' : ??T";
   7.214 +    have t: "?t : ?T"; by (rule dominoes_tile_matrix);
   7.215 +    assume t'': "?t'' : ?T";
   7.216  
   7.217 -    let ??e = evnodd;
   7.218 -    have fin: "finite (??e ??t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
   7.219 +    let ?e = evnodd;
   7.220 +    have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
   7.221  
   7.222      note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
   7.223 -    have "card (??e ??t'' 0) < card (??e ??t' 0)";
   7.224 +    have "card (?e ?t'' 0) < card (?e ?t' 0)";
   7.225      proof -;
   7.226 -      have "card (??e ??t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (??e ??t' 0)";
   7.227 +      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)";
   7.228        proof (rule card_Diff1_less);
   7.229 -	show "finite (??e ??t' 0)"; by (rule finite_subset, rule fin) force;
   7.230 -	show "(2 * m + 1, 2 * n + 1) : ??e ??t' 0"; by simp;
   7.231 +	show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force;
   7.232 +	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
   7.233        qed;
   7.234 -      thus ??thesis; by simp;
   7.235 +      thus ?thesis; by simp;
   7.236      qed;
   7.237 -    also; have "... < card (??e ??t 0)";
   7.238 +    also; have "... < card (?e ?t 0)";
   7.239      proof -;
   7.240 -      have "(0, 0) : ??e ??t 0"; by simp;
   7.241 -      with fin; have "card (??e ??t 0 - {(0, 0)}) < card (??e ??t 0)"; by (rule card_Diff1_less);
   7.242 -      thus ??thesis; by simp;
   7.243 +      have "(0, 0) : ?e ?t 0"; by simp;
   7.244 +      with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less);
   7.245 +      thus ?thesis; by simp;
   7.246      qed;
   7.247 -    also; from t; have "... = card (??e ??t 1)"; by (rule tiling_domino_01);
   7.248 -    also; have "??e ??t 1 = ??e ??t'' 1"; by simp;
   7.249 -    also; from t''; have "card ... = card (??e ??t'' 0)"; by (rule tiling_domino_01 [RS sym]);
   7.250 +    also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
   7.251 +    also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
   7.252 +    also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]);
   7.253      finally; show False; ..;
   7.254    qed;
   7.255  qed;
     8.1 --- a/src/HOL/Isar_examples/Summation.thy	Sat Sep 04 21:12:15 1999 +0200
     8.2 +++ b/src/HOL/Isar_examples/Summation.thy	Sat Sep 04 21:13:01 1999 +0200
     8.3 @@ -46,51 +46,51 @@
     8.4  
     8.5  
     8.6  theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
     8.7 -  (is "??P n" is "??S n = _");
     8.8 +  (is "?P n" is "?S n = _");
     8.9  proof (induct n);
    8.10 -  show "??P 0"; by simp;
    8.11 +  show "?P 0"; by simp;
    8.12  
    8.13    fix n;
    8.14 -  have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp;
    8.15 -  also; assume "??S n = n * (n + 1)";
    8.16 +  have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
    8.17 +  also; assume "?S n = n * (n + 1)";
    8.18    also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
    8.19 -  finally; show "??P (Suc n)"; by simp;
    8.20 +  finally; show "?P (Suc n)"; by simp;
    8.21  qed;
    8.22  
    8.23  theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
    8.24 -  (is "??P n" is "??S n = _");
    8.25 +  (is "?P n" is "?S n = _");
    8.26  proof (induct n);
    8.27 -  show "??P 0"; by simp;
    8.28 +  show "?P 0"; by simp;
    8.29  
    8.30    fix n;
    8.31 -  have "??S (n + 1) = ??S n + 2 * n + 1"; by simp;
    8.32 -  also; assume "??S n = n^2";
    8.33 +  have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
    8.34 +  also; assume "?S n = n^2";
    8.35    also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
    8.36 -  finally; show "??P (Suc n)"; by simp;
    8.37 +  finally; show "?P (Suc n)"; by simp;
    8.38  qed;
    8.39  
    8.40  theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
    8.41 -  (is "??P n" is "??S n = _");
    8.42 +  (is "?P n" is "?S n = _");
    8.43  proof (induct n);
    8.44 -  show "??P 0"; by simp;
    8.45 +  show "?P 0"; by simp;
    8.46  
    8.47    fix n;
    8.48 -  have "??S (n + 1) = ??S n + 6 * (n + 1)^2"; by simp;
    8.49 -  also; assume "??S n = n * (n + 1) * (2 * n + 1)";
    8.50 +  have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
    8.51 +  also; assume "?S n = n * (n + 1) * (2 * n + 1)";
    8.52    also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
    8.53 -  finally; show "??P (Suc n)"; by simp;
    8.54 +  finally; show "?P (Suc n)"; by simp;
    8.55  qed;
    8.56  
    8.57  theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
    8.58 -  (is "??P n" is "??S n = _");
    8.59 +  (is "?P n" is "?S n = _");
    8.60  proof (induct n);
    8.61 -  show "??P 0"; by simp;
    8.62 +  show "?P 0"; by simp;
    8.63  
    8.64    fix n;
    8.65 -  have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp;
    8.66 -  also; assume "??S n = (n * (n + 1))^2";
    8.67 +  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
    8.68 +  also; assume "?S n = (n * (n + 1))^2";
    8.69    also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
    8.70 -  finally; show "??P (Suc n)"; by simp;
    8.71 +  finally; show "?P (Suc n)"; by simp;
    8.72  qed;
    8.73  
    8.74  
     9.1 --- a/src/HOL/ex/Points.thy	Sat Sep 04 21:12:15 1999 +0200
     9.2 +++ b/src/HOL/ex/Points.thy	Sat Sep 04 21:13:01 1999 +0200
     9.3 @@ -94,9 +94,9 @@
     9.4  
     9.5  text {* equality of records *};
     9.6  
     9.7 -lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _");
     9.8 +lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "?EQ --> _");
     9.9  proof;
    9.10 -  assume ??EQ;
    9.11 +  assume ?EQ;
    9.12    thus "n = n'"; by simp;
    9.13  qed;
    9.14