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