# HG changeset patch
# User wenzelm
# Date 931451974 -7200
# Node ID c7c365b4f6151dd942d87bddc275f2c90f1b5699
# Parent  914233d95b23160cd7f31aeee72fafd3a6f617d2
removed old version;
tuned;

diff -r 914233d95b23 -r c7c365b4f615 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Thu Jul 08 18:39:08 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Thu Jul 08 18:39:34 1999 +0200
@@ -12,7 +12,7 @@
 theorems [dest] = monoD;  (* FIXME [dest!!] *)
 
 text {*
- The proofs of Knaster-Tarski below closely follows the presentation in
+ The proof of Knaster-Tarski below closely follows the presentation in
  'Introduction to Lattices' and Order by Davey/Priestley, pages
  93--94.  All of their narration has been rephrased in terms of formal
  Isar language elements.  Just as many textbook-style proofs, there is
@@ -20,7 +20,7 @@
  structure.
 *};
 
-theorem KnasterTarski1: "mono f ==> EX a::'a set. f a = a";
+theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
 proof;
   let ??H = "{u. f u <= u}";
   let ??a = "Inter ??H";
@@ -34,34 +34,7 @@
       hence "??a <= x"; by (rule Inter_lower);
       with mono; have "f ??a <= f x"; ..;
       also; from mem; have "... <= x"; ..;
-      finally (order_trans); have "f ??a <= x"; .;
-    }};
-    hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
-    thus ??thesis;
-    proof (rule order_antisym);
-      from mono ge; have "f (f ??a) <= f ??a"; ..;
-      hence "f ??a : ??H"; ..;
-      thus "??a <= f ??a"; by (rule Inter_lower);
-    qed;
-  qed;
-qed;
-
-
-theorem KnasterTarski2: "mono f ==> EX a::'a set. f a = a";
-proof;
-  let ??H = "{u. f u <= u}";
-  let ??a = "Inter ??H";
-
-  assume mono: "mono f";
-  show "f ??a = ??a";
-  proof same;
-    {{;
-      fix x;
-      assume mem: "x : ??H";
-      hence "??a <= x"; by (rule Inter_lower);
-      with mono; have "f ??a <= f x"; ..;
-      also; from mem; have "... <= x"; ..;
-      finally (order_trans); have "f ??a <= x"; .;
+      finally; have "f ??a <= x"; .;
     }};
     hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
     {{;