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;