# HG changeset patch
# User wenzelm
# Date 930860458 -7200
# Node ID f898679685b76a954a66c78cfcd7895ca5b45855
# Parent  fe4e3d26fa8f64fa771314e4f01d276fdefe1054
fixed order_trans;

diff -r fe4e3d26fa8f -r f898679685b7 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Thu Jul 01 21:30:18 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Thu Jul 01 22:20:58 1999 +0200
@@ -8,21 +8,18 @@
 
 theory KnasterTarski = Main:;
 
-(*
+
+theorems [dest] = monoD;  (* FIXME [dest!!] *)
 
-text {*
+(*
  The proof of Knaster-Tarski below closely follows the presentation in
- 'Introduction to Lattices and Order' by Davey/Priestley, pages
+ 'Introduction to Lattices' and Order by Davey/Priestley, pages
  93--94.  Only one statement of their narration has not been rephrased
  in formal Isar language elements, but left as a comment.  Also note
  that Davey/Priestley do not point out non-emptyness of the set ??H,
  (which is obvious, but not vacous).
-*};
 *)
 
-theorems [dest] = monoD;  (* FIXME [dest!!] *)
-
-
 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
 proof;
   let ??H = "{u. f u <= u}";
@@ -36,15 +33,15 @@
     hence "??a <= x"; by (rule Inter_lower);
     with mono; have "f ??a <= f x"; ..;
     also; from mem; have "f x <= x"; ..;
-    finally; have "f ??a <= x"; .;
+    finally (order_trans); have "f ??a <= x"; .;
     hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
     (* text {* We now use this inequality to prove the reverse one (!)
       and thereby complete the proof that @term{??a} is a fixpoint. *};  *)
     with mono; have "f (f ??a) <= f ??a"; ..;
     hence "f ??a : ??H"; ..;
     hence "??a <= f ??a"; by (rule Inter_lower);
-    also (order_antisym); note ge;
-    finally; show "f ??a = ??a"; proof same;
+    also; note ge;
+    finally; show "f ??a = ??a"; by (rule sym);
   next;
     have "f UNIV <= UNIV"; by (rule subset_UNIV);
     thus "UNIV : ??H"; ..;