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;