src/HOL/Isar_examples/KnasterTarski.thy
changeset 7480 0a0e0dbe1269
parent 7253 a494a78fea39
child 7761 7fab9592384f
     1.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Sat Sep 04 21:12:15 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sat Sep 04 21:13:01 1999 +0200
     1.3 @@ -37,28 +37,28 @@
     1.4  
     1.5  theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
     1.6  proof;
     1.7 -  let ??H = "{u. f u <= u}";
     1.8 -  let ??a = "Inter ??H";
     1.9 +  let ?H = "{u. f u <= u}";
    1.10 +  let ?a = "Inter ?H";
    1.11  
    1.12    assume mono: "mono f";
    1.13 -  show "f ??a = ??a";
    1.14 +  show "f ?a = ?a";
    1.15    proof -;
    1.16      {{;
    1.17        fix x;
    1.18 -      assume mem: "x : ??H";
    1.19 -      hence "??a <= x"; by (rule Inter_lower);
    1.20 -      with mono; have "f ??a <= f x"; ..;
    1.21 +      assume mem: "x : ?H";
    1.22 +      hence "?a <= x"; by (rule Inter_lower);
    1.23 +      with mono; have "f ?a <= f x"; ..;
    1.24        also; from mem; have "... <= x"; ..;
    1.25 -      finally; have "f ??a <= x"; .;
    1.26 +      finally; have "f ?a <= x"; .;
    1.27      }};
    1.28 -    hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
    1.29 +    hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
    1.30      {{;
    1.31 -      also; presume "... <= f ??a";
    1.32 -      finally (order_antisym); show ??thesis; .;
    1.33 +      also; presume "... <= f ?a";
    1.34 +      finally (order_antisym); show ?thesis; .;
    1.35      }};
    1.36 -    from mono ge; have "f (f ??a) <= f ??a"; ..;
    1.37 -    hence "f ??a : ??H"; ..;
    1.38 -    thus "??a <= f ??a"; by (rule Inter_lower);
    1.39 +    from mono ge; have "f (f ?a) <= f ?a"; ..;
    1.40 +    hence "f ?a : ?H"; ..;
    1.41 +    thus "?a <= f ?a"; by (rule Inter_lower);
    1.42    qed;
    1.43  qed;
    1.44