src/HOL/Isar_examples/Cantor.thy
 changeset 7480 0a0e0dbe1269 parent 6746 cf6ad8d22793 child 7748 5b9c45b21782
```     1.1 --- a/src/HOL/Isar_examples/Cantor.thy	Sat Sep 04 21:12:15 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Sat Sep 04 21:13:01 1999 +0200
1.3 @@ -34,25 +34,25 @@
1.4
1.5  theorem "EX S. S ~: range(f :: 'a => 'a set)";
1.6  proof;
1.7 -  let ??S = "{x. x ~: f x}";
1.8 -  show "??S ~: range f";
1.9 +  let ?S = "{x. x ~: f x}";
1.10 +  show "?S ~: range f";
1.11    proof;
1.12 -    assume "??S : range f";
1.13 +    assume "?S : range f";
1.14      then; show False;
1.15      proof;
1.16        fix y;
1.17 -      assume "??S = f y";
1.18 -      then; show ??thesis;
1.19 +      assume "?S = f y";
1.20 +      then; show ?thesis;
1.21        proof (rule equalityCE);
1.22 -        assume y_in_S: "y : ??S";
1.23 +        assume y_in_S: "y : ?S";
1.24          assume y_in_fy: "y : f y";
1.25          from y_in_S; have y_notin_fy: "y ~: f y"; ..;
1.26 -        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
1.27 +        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
1.28        next;
1.29 -        assume y_notin_S: "y ~: ??S";
1.30 +        assume y_notin_S: "y ~: ?S";
1.31          assume y_notin_fy: "y ~: f y";
1.32          from y_notin_S; have y_in_fy: "y : f y"; ..;
1.33 -        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
1.34 +        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
1.35        qed;
1.36      qed;
1.37    qed;
1.38 @@ -67,23 +67,23 @@
1.39
1.40  theorem "EX S. S ~: range(f :: 'a => 'a set)";
1.41  proof;
1.42 -  let ??S = "{x. x ~: f x}";
1.43 -  show "??S ~: range f";
1.44 +  let ?S = "{x. x ~: f x}";
1.45 +  show "?S ~: range f";
1.46    proof;
1.47 -    assume "??S : range f";
1.48 +    assume "?S : range f";
1.49      thus False;
1.50      proof;
1.51        fix y;
1.52 -      assume "??S = f y";
1.53 -      thus ??thesis;
1.54 +      assume "?S = f y";
1.55 +      thus ?thesis;
1.56        proof (rule equalityCE);
1.57          assume "y : f y";
1.58 -        assume "y : ??S"; hence "y ~: f y"; ..;
1.59 -        thus ??thesis; by contradiction;
1.60 +        assume "y : ?S"; hence "y ~: f y"; ..;
1.61 +        thus ?thesis; by contradiction;
1.62        next;
1.63          assume "y ~: f y";
1.64 -        assume "y ~: ??S"; hence "y : f y"; ..;
1.65 -        thus ??thesis; by contradiction;
1.66 +        assume "y ~: ?S"; hence "y : f y"; ..;
1.67 +        thus ?thesis; by contradiction;
1.68        qed;
1.69      qed;
1.70    qed;
```