--- a/src/HOL/Isar_examples/KnasterTarski.thy Sat Jul 03 00:26:00 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Sat Jul 03 00:28:05 1999 +0200
@@ -11,7 +11,7 @@
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
93--94. All of their narration has been rephrased in terms of formal
@@ -22,7 +22,7 @@
Just as many textbook-style proofs, there is a strong bias towards
forward reasoning, with little hierarchical structure.
-*)
+*};
theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
proof;