# HG changeset patch
# User wenzelm
# Date 930954485 -7200
# Node ID 6e56603fb33942e8041d8513b23cb2695488755e
# Parent  4a905b4a39c8cb58d8e244550f19fef8c4ff7626
proper text;

diff -r 4a905b4a39c8 -r 6e56603fb339 src/HOL/Isar_examples/KnasterTarski.thy
--- 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;