# HG changeset patch
# User wenzelm
# Date 936472381 -7200
# Node ID 0a0e0dbe1269e1e8def7381f2d941a0399a9e25a
# Parent  b482d827899c0c82edd1ad8d05c6b6f00c74bfe3
replaced ?? by ?;

diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -80,7 +80,7 @@
   then; show "B & A";
   proof;
     assume A B;
-    show ??thesis; ..;
+    show ?thesis; ..;
   qed;
 qed;
 
@@ -123,8 +123,8 @@
   then; show "EX x. P(x)";
   proof (rule exE);
     fix a;
-    assume "P(f(a))" (is "P(??witness)");
-    show ??thesis; by (rule exI [of P ??witness]);
+    assume "P(f(a))" (is "P(?witness)");
+    show ?thesis; by (rule exI [of P ?witness]);
   qed;
 qed;
 
@@ -135,7 +135,7 @@
   proof;
     fix a;
     assume "P(f(a))";
-    show ??thesis; ..;
+    show ?thesis; ..;
   qed;
 qed;
 
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -34,25 +34,25 @@
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
 proof;
-  let ??S = "{x. x ~: f x}";
-  show "??S ~: range f";
+  let ?S = "{x. x ~: f x}";
+  show "?S ~: range f";
   proof;
-    assume "??S : range f";
+    assume "?S : range f";
     then; show False;
     proof;
       fix y; 
-      assume "??S = f y";
-      then; show ??thesis;
+      assume "?S = f y";
+      then; show ?thesis;
       proof (rule equalityCE);
-        assume y_in_S: "y : ??S";
+        assume y_in_S: "y : ?S";
         assume y_in_fy: "y : f y";
         from y_in_S; have y_notin_fy: "y ~: f y"; ..;
-        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
+        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
       next;
-        assume y_notin_S: "y ~: ??S";
+        assume y_notin_S: "y ~: ?S";
         assume y_notin_fy: "y ~: f y";
         from y_notin_S; have y_in_fy: "y : f y"; ..;
-        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
+        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
       qed;
     qed;
   qed;
@@ -67,23 +67,23 @@
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
 proof;
-  let ??S = "{x. x ~: f x}";
-  show "??S ~: range f";
+  let ?S = "{x. x ~: f x}";
+  show "?S ~: range f";
   proof;
-    assume "??S : range f";
+    assume "?S : range f";
     thus False;
     proof;
       fix y; 
-      assume "??S = f y";
-      thus ??thesis;
+      assume "?S = f y";
+      thus ?thesis;
       proof (rule equalityCE);
         assume "y : f y";
-        assume "y : ??S"; hence "y ~: f y"; ..;
-        thus ??thesis; by contradiction;
+        assume "y : ?S"; hence "y ~: f y"; ..;
+        thus ?thesis; by contradiction;
       next;
         assume "y ~: f y";
-        assume "y ~: ??S"; hence "y : f y"; ..;
-        thus ??thesis; by contradiction;
+        assume "y ~: ?S"; hence "y : f y"; ..;
+        thus ?thesis; by contradiction;
       qed;
     qed;
   qed;
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -100,30 +100,30 @@
 *};
 
 lemma exec_append:
-  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
-proof (induct ??P xs type: list);
-  show "??P []"; by simp;
+  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs");
+proof (induct ?P xs type: list);
+  show "?P []"; by simp;
 
   fix x xs;
-  assume "??P xs";
-  show "??P (x # xs)" (is "??Q x");
-  proof (induct ??Q x type: instr);
-    fix val; show "??Q (Const val)"; by force;
+  assume "?P xs";
+  show "?P (x # xs)" (is "?Q x");
+  proof (induct ?Q x type: instr);
+    fix val; show "?Q (Const val)"; by force;
   next;
-    fix adr; show "??Q (Load adr)"; by force;
+    fix adr; show "?Q (Load adr)"; by force;
   next;
-    fix fun; show "??Q (Apply fun)"; by force;
+    fix fun; show "?Q (Apply fun)"; by force;
   qed;
 qed;
 
 lemma exec_comp:
-  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
-proof (induct ??P e type: expr);
-  fix adr; show "??P (Variable adr)"; by force;
+  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
+proof (induct ?P e type: expr);
+  fix adr; show "?P (Variable adr)"; by force;
 next;
-  fix val; show "??P (Constant val)"; by force;
+  fix val; show "?P (Constant val)"; by force;
 next;
-  fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
+  fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
     by (force simp add: exec_append);
 qed;
 
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/Group.thy
--- a/src/HOL/Isar_examples/Group.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -49,7 +49,7 @@
     by (simp only: group_left_unit);
   also; have "... = one";
     by (simp only: group_left_inverse);
-  finally; show ??thesis; .;
+  finally; show ?thesis; .;
 qed;
 
 text {*
@@ -67,7 +67,7 @@
     by (simp only: group_right_inverse);
   also; have "... = x";
     by (simp only: group_left_unit);
-  finally; show ??thesis; .;
+  finally; show ?thesis; .;
 qed;
 
 text {*
@@ -80,7 +80,7 @@
 
  Note that "..." is just a special term binding that happens to be
  bound automatically to the argument of the last fact established by
- assume or any local goal.  In contrast to ??thesis, "..." is bound
+ assume or any local goal.  In contrast to ?thesis, "..." is bound
  after the proof is finished.
 *};
 
@@ -112,7 +112,7 @@
   from calculation
     -- {* ... and pick up final result *};
 
-  show ??thesis; .;
+  show ?thesis; .;
 qed;
 
 
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -37,28 +37,28 @@
 
 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
 proof;
-  let ??H = "{u. f u <= u}";
-  let ??a = "Inter ??H";
+  let ?H = "{u. f u <= u}";
+  let ?a = "Inter ?H";
 
   assume mono: "mono f";
-  show "f ??a = ??a";
+  show "f ?a = ?a";
   proof -;
     {{;
       fix x;
-      assume mem: "x : ??H";
-      hence "??a <= x"; by (rule Inter_lower);
-      with mono; have "f ??a <= f x"; ..;
+      assume mem: "x : ?H";
+      hence "?a <= x"; by (rule Inter_lower);
+      with mono; have "f ?a <= f x"; ..;
       also; from mem; have "... <= x"; ..;
-      finally; have "f ??a <= x"; .;
+      finally; have "f ?a <= x"; .;
     }};
-    hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
+    hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
     {{;
-      also; presume "... <= f ??a";
-      finally (order_antisym); show ??thesis; .;
+      also; presume "... <= f ?a";
+      finally (order_antisym); show ?thesis; .;
     }};
-    from mono ge; have "f (f ??a) <= f ??a"; ..;
-    hence "f ??a : ??H"; ..;
-    thus "??a <= f ??a"; by (rule Inter_lower);
+    from mono ge; have "f (f ?a) <= f ?a"; ..;
+    hence "f ?a : ?H"; ..;
+    thus "?a <= f ?a"; by (rule Inter_lower);
   qed;
 qed;
 
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -14,50 +14,50 @@
 
 lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
 proof;
-  let ??R = "mult1 r";
-  let ??W = "acc ??R";
+  let ?R = "mult1 r";
+  let ?W = "acc ?R";
 
 
   {{;
     fix M M0 a;
-    assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)"
-      and M0: "M0 : ??W"
-      and acc_hyp: "ALL M. (M, M0) : ??R --> M + {#a#} : ??W";
-    have "M0 + {#a#} : ??W";
+    assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
+      and M0: "M0 : ?W"
+      and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
+    have "M0 + {#a#} : ?W";
     proof (rule accI [of "M0 + {#a#}"]);
-      fix N; assume "(N, M0 + {#a#}) : ??R";
-      hence "((EX M. (M, M0) : ??R & N = M + {#a#}) |
+      fix N; assume "(N, M0 + {#a#}) : ?R";
+      hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
              (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
 	by (simp only: less_add_conv);
-      thus "N : ??W";
+      thus "N : ?W";
       proof (elim exE disjE conjE);
-	fix M; assume "(M, M0) : ??R" and N: "N = M + {#a#}";
-	from acc_hyp; have "(M, M0) : ??R --> M + {#a#} : ??W"; ..;
-	hence "M + {#a#} : ??W"; ..;
-	thus "N : ??W"; by (simp only: N);
+	fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}";
+	from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..;
+	hence "M + {#a#} : ?W"; ..;
+	thus "N : ?W"; by (simp only: N);
       next;
 	fix K;
 	assume N: "N = M0 + K";
 	assume "ALL b. elem K b --> (b, a) : r";
-	have "??this --> M0 + K : ??W" (is "??P K");
+	have "?this --> M0 + K : ?W" (is "?P K");
 	proof (rule multiset_induct [of _ K]);
-	  from M0; have "M0 + {#} : ??W"; by simp;
-	  thus "??P {#}"; ..;
+	  from M0; have "M0 + {#} : ?W"; by simp;
+	  thus "?P {#}"; ..;
 
-	  fix K x; assume hyp: "??P K";
-	  show "??P (K + {#x#})";
+	  fix K x; assume hyp: "?P K";
+	  show "?P (K + {#x#})";
 	  proof;
 	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
 	    hence "(x, a) : r"; by simp;
-	    with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..;
+	    with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..;
 
-	    from a hyp; have "M0 + K : ??W"; by simp;
-	    with b; have "(M0 + K) + {#x#} : ??W"; ..;
-	    thus "M0 + (K + {#x#}) : ??W"; by (simp only: union_assoc);
+	    from a hyp; have "M0 + K : ?W"; by simp;
+	    with b; have "(M0 + K) + {#x#} : ?W"; ..;
+	    thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc);
 	  qed;
 	qed;
-	hence "M0 + K : ??W"; ..;
-	thus "N : ??W"; by (simp only: N);
+	hence "M0 + K : ?W"; ..;
+	thus "N : ?W"; by (simp only: N);
       qed;
     qed;
   }}; note tedious_reasoning = this;
@@ -65,25 +65,25 @@
 
   assume wf: "wf r";
   fix M;
-  show "M : ??W";
+  show "M : ?W";
   proof (rule multiset_induct [of _ M]);
-    show "{#} : ??W";
+    show "{#} : ?W";
     proof (rule accI);
-      fix b; assume "(b, {#}) : ??R";
-      with not_less_empty; show "b : ??W"; by contradiction;
+      fix b; assume "(b, {#}) : ?R";
+      with not_less_empty; show "b : ?W"; by contradiction;
     qed;
 
-    fix M a; assume "M : ??W";
-    from wf; have "ALL M:??W. M + {#a#} : ??W";
+    fix M a; assume "M : ?W";
+    from wf; have "ALL M:?W. M + {#a#} : ?W";
     proof (rule wf_induct [of r]);
-      fix a; assume "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)";
-      show "ALL M:??W. M + {#a#} : ??W";
+      fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
+      show "ALL M:?W. M + {#a#} : ?W";
       proof;
-	fix M; assume "M : ??W";
-	thus "M + {#a#} : ??W"; by (rule acc_induct) (rule tedious_reasoning);
+	fix M; assume "M : ?W";
+	thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning);
       qed;
     qed;
-    thus "M + {#a#} : ??W"; ..;
+    thus "M + {#a#} : ?W"; ..;
   qed;
 qed;
 
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -28,21 +28,21 @@
 
 lemma tiling_Un: "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
 proof;
-  assume "t : tiling A" (is "_ : ??T");
-  thus "u : ??T --> t Int u = {} --> t Un u : ??T" (is "??P t");
+  assume "t : tiling A" (is "_ : ?T");
+  thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
   proof (induct t set: tiling);
-    show "??P {}"; by simp;
+    show "?P {}"; by simp;
 
     fix a t;
-    assume "a : A" "t : ??T" "??P t" "a <= - t";
-    show "??P (a Un t)";
+    assume "a : A" "t : ?T" "?P t" "a <= - t";
+    show "?P (a Un t)";
     proof (intro impI);
-      assume "u : ??T" "(a Un t) Int u = {}";
-      have hyp: "t Un u: ??T"; by blast;
+      assume "u : ?T" "(a Un t) Int u = {}";
+      have hyp: "t Un u: ?T"; by blast;
       have "a <= - (t Un u)"; by blast;
-      with _ hyp; have "a Un (t Un u) : ??T"; by (rule tiling.Un);
+      with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
       also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
-      finally; show "... : ??T"; .;
+      finally; show "... : ?T"; .;
     qed;
   qed;
 qed;
@@ -113,41 +113,41 @@
 
 
 lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
-  (is "??P n" is "??B n : ??T");
+  (is "?P n" is "?B n : ?T");
 proof (induct n);
-  show "??P 0"; by (simp add: below_0 tiling.empty);
+  show "?P 0"; by (simp add: below_0 tiling.empty);
 
-  fix n; assume hyp: "??P n";
-  let ??a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
+  fix n; assume hyp: "?P n";
+  let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
 
-  have "??B (Suc n) = ??a Un ??B n"; by (simp add: Sigma_Suc Un_assoc);
-  also; have "... : ??T";
+  have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
+  also; have "... : ?T";
   proof (rule tiling.Un);
     have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz);
-    also; have "{(i, 2 * n), (i, 2 * n + 1)} = ??a"; by blast;
+    also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast;
     finally; show "... : domino"; .;
-    from hyp; show "??B n : ??T"; .;
-    show "??a <= - ??B n"; by force;
+    from hyp; show "?B n : ?T"; .;
+    show "?a <= - ?B n"; by force;
   qed;
-  finally; show "??P (Suc n)"; .;
+  finally; show "?P (Suc n)"; .;
 qed;
 
 lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino"
-  (is "??P m" is "??B m : ??T");
+  (is "?P m" is "?B m : ?T");
 proof (induct m);
-  show "??P 0"; by (simp add: below_0 tiling.empty);
+  show "?P 0"; by (simp add: below_0 tiling.empty);
 
-  fix m; assume hyp: "??P m";
-  let ??t = "{m} Times below (2 * n)";
+  fix m; assume hyp: "?P m";
+  let ?t = "{m} Times below (2 * n)";
 
-  have "??B (Suc m) = ??t Un ??B m"; by (simp add: Sigma_Suc);
-  also; have "... : ??T";
+  have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
+  also; have "... : ?T";
   proof (rule tiling_Un [rulify]);
-    show "??t : ??T"; by (rule dominoes_tile_row);
-    from hyp; show "??B m : ??T"; .;
-    show "??t Int ??B m = {}"; by blast;
+    show "?t : ?T"; by (rule dominoes_tile_row);
+    from hyp; show "?B m : ?T"; .;
+    show "?t Int ?B m = {}"; by blast;
   qed;
-  finally; show "??P (Suc m)"; .;
+  finally; show "?P (Suc m)"; .;
 qed;
 
 
@@ -155,13 +155,13 @@
 proof -;
   assume "b < 2";
   assume "d : domino";
-  thus ??thesis (is "??P d");
+  thus ?thesis (is "?P d");
   proof (induct d set: domino);
     have b_cases: "b = 0 | b = 1"; by arith;
     fix i j;
     note [simp] = evnodd_empty evnodd_insert mod_Suc;
-    from b_cases; show "??P {(i, j), (i, j + 1)}"; by rule auto;
-    from b_cases; show "??P {(i, j), (i + 1, j)}"; by rule auto;
+    from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
+    from b_cases; show "?P {(i, j), (i + 1, j)}"; by rule auto;
   qed;
 qed;
 
@@ -175,54 +175,54 @@
 
 section {* Tilings of dominoes *};
 
-lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ??T ==> ??F t");
+lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
 proof -;
-  assume "t : ??T";
-  thus "??F t";
+  assume "t : ?T";
+  thus "?F t";
   proof (induct t set: tiling);
-    show "??F {}"; by (rule Finites.emptyI);
-    fix a t; assume "??F t";
-    assume "a : domino"; hence "??F a"; by (rule domino_finite);
-    thus "??F (a Un t)"; by (rule finite_UnI);
+    show "?F {}"; by (rule Finites.emptyI);
+    fix a t; assume "?F t";
+    assume "a : domino"; hence "?F a"; by (rule domino_finite);
+    thus "?F (a Un t)"; by (rule finite_UnI);
   qed;
 qed;
 
 lemma tiling_domino_01: "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
-  (is "t : ??T ==> ??P t");
+  (is "t : ?T ==> ?P t");
 proof -;
-  assume "t : ??T";
-  thus "??P t";
+  assume "t : ?T";
+  thus "?P t";
   proof (induct t set: tiling);
-    show "??P {}"; by (simp add: evnodd_def);
+    show "?P {}"; by (simp add: evnodd_def);
 
     fix a t;
-    let ??e = evnodd;
-    assume "a : domino" "t : ??T"
-      and hyp: "card (??e t 0) = card (??e t 1)"
+    let ?e = evnodd;
+    assume "a : domino" "t : ?T"
+      and hyp: "card (?e t 0) = card (?e t 1)"
       and "a <= - t";
 
-    have card_suc: "!!b. b < 2 ==> card (??e (a Un t) b) = Suc (card (??e t b))";
+    have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
     proof -;
       fix b; assume "b < 2";
-      have "EX i j. ??e a b = {(i, j)}"; by (rule domino_singleton);
-      thus "??thesis b";
+      have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
+      thus "?thesis b";
       proof (elim exE);
-	have "??e (a Un t) b = ??e a b Un ??e t b"; by (rule evnodd_Un);
-	also; fix i j; assume "??e a b = {(i, j)}";
-	also; have "... Un ??e t b = insert (i, j) (??e t b)"; by simp;
-	also; have "card ... = Suc (card (??e t b))";
+	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
+	also; fix i j; assume "?e a b = {(i, j)}";
+	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
+	also; have "card ... = Suc (card (?e t b))";
 	proof (rule card_insert_disjoint);
-	  show "finite (??e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
-	  have "(i, j) : ??e a b"; by asm_simp;
-	  thus "(i, j) ~: ??e t b"; by (force dest: evnoddD);
+	  show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
+	  have "(i, j) : ?e a b"; by asm_simp;
+	  thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
 	qed;
-	finally; show ??thesis; .;
+	finally; show ?thesis; .;
       qed;
     qed;
-    hence "card (??e (a Un t) 0) = Suc (card (??e t 0))"; by simp;
-    also; from hyp; have "card (??e t 0) = card (??e t 1)"; .;
-    also; from card_suc; have "Suc ... = card (??e (a Un t) 1)"; by simp;
-    finally; show "??P (a Un t)"; .;
+    hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp;
+    also; from hyp; have "card (?e t 0) = card (?e t 1)"; .;
+    also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp;
+    finally; show "?P (a Un t)"; .;
   qed;
 qed;
 
@@ -236,37 +236,37 @@
 
 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
 proof (unfold mutilated_board_def);
-  let ??T = "tiling domino";
-  let ??t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
-  let ??t' = "??t - {(0, 0)}";
-  let ??t'' = "??t' - {(2 * m + 1, 2 * n + 1)}";
-  show "??t'' ~: ??T";
+  let ?T = "tiling domino";
+  let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
+  let ?t' = "?t - {(0, 0)}";
+  let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
+  show "?t'' ~: ?T";
   proof;
-    have t: "??t : ??T"; by (rule dominoes_tile_matrix);
-    assume t'': "??t'' : ??T";
+    have t: "?t : ?T"; by (rule dominoes_tile_matrix);
+    assume t'': "?t'' : ?T";
 
-    let ??e = evnodd;
-    have fin: "finite (??e ??t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
+    let ?e = evnodd;
+    have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
 
     note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
-    have "card (??e ??t'' 0) < card (??e ??t' 0)";
+    have "card (?e ?t'' 0) < card (?e ?t' 0)";
     proof -;
-      have "card (??e ??t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (??e ??t' 0)";
+      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)";
       proof (rule card_Diff1_less);
-	show "finite (??e ??t' 0)"; by (rule finite_subset, rule fin) force;
-	show "(2 * m + 1, 2 * n + 1) : ??e ??t' 0"; by simp;
+	show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force;
+	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
       qed;
-      thus ??thesis; by simp;
+      thus ?thesis; by simp;
     qed;
-    also; have "... < card (??e ??t 0)";
+    also; have "... < card (?e ?t 0)";
     proof -;
-      have "(0, 0) : ??e ??t 0"; by simp;
-      with fin; have "card (??e ??t 0 - {(0, 0)}) < card (??e ??t 0)"; by (rule card_Diff1_less);
-      thus ??thesis; by simp;
+      have "(0, 0) : ?e ?t 0"; by simp;
+      with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less);
+      thus ?thesis; by simp;
     qed;
-    also; from t; have "... = card (??e ??t 1)"; by (rule tiling_domino_01);
-    also; have "??e ??t 1 = ??e ??t'' 1"; by simp;
-    also; from t''; have "card ... = card (??e ??t'' 0)"; by (rule tiling_domino_01 [RS sym]);
+    also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
+    also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
+    also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]);
     finally; show False; ..;
   qed;
 qed;
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -46,51 +46,51 @@
 
 
 theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
-  (is "??P n" is "??S n = _");
+  (is "?P n" is "?S n = _");
 proof (induct n);
-  show "??P 0"; by simp;
+  show "?P 0"; by simp;
 
   fix n;
-  have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp;
-  also; assume "??S n = n * (n + 1)";
+  have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
+  also; assume "?S n = n * (n + 1)";
   also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
-  finally; show "??P (Suc n)"; by simp;
+  finally; show "?P (Suc n)"; by simp;
 qed;
 
 theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
-  (is "??P n" is "??S n = _");
+  (is "?P n" is "?S n = _");
 proof (induct n);
-  show "??P 0"; by simp;
+  show "?P 0"; by simp;
 
   fix n;
-  have "??S (n + 1) = ??S n + 2 * n + 1"; by simp;
-  also; assume "??S n = n^2";
+  have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
+  also; assume "?S n = n^2";
   also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
-  finally; show "??P (Suc n)"; by simp;
+  finally; show "?P (Suc n)"; by simp;
 qed;
 
 theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
-  (is "??P n" is "??S n = _");
+  (is "?P n" is "?S n = _");
 proof (induct n);
-  show "??P 0"; by simp;
+  show "?P 0"; by simp;
 
   fix n;
-  have "??S (n + 1) = ??S n + 6 * (n + 1)^2"; by simp;
-  also; assume "??S n = n * (n + 1) * (2 * n + 1)";
+  have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
+  also; assume "?S n = n * (n + 1) * (2 * n + 1)";
   also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
-  finally; show "??P (Suc n)"; by simp;
+  finally; show "?P (Suc n)"; by simp;
 qed;
 
 theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
-  (is "??P n" is "??S n = _");
+  (is "?P n" is "?S n = _");
 proof (induct n);
-  show "??P 0"; by simp;
+  show "?P 0"; by simp;
 
   fix n;
-  have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp;
-  also; assume "??S n = (n * (n + 1))^2";
+  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
+  also; assume "?S n = (n * (n + 1))^2";
   also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
-  finally; show "??P (Suc n)"; by simp;
+  finally; show "?P (Suc n)"; by simp;
 qed;
 
 
diff -r b482d827899c -r 0a0e0dbe1269 src/HOL/ex/Points.thy
--- a/src/HOL/ex/Points.thy	Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/ex/Points.thy	Sat Sep 04 21:13:01 1999 +0200
@@ -94,9 +94,9 @@
 
 text {* equality of records *};
 
-lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _");
+lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "?EQ --> _");
 proof;
-  assume ??EQ;
+  assume ?EQ;
   thus "n = n'"; by simp;
 qed;