--- 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;