src/HOL/Isar_examples/KnasterTarski.thy

 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
  93--94.  All of their narration has been rephrased in terms of formal
  Isar language elements, except one stament only that has been left as
  a comment.  Also note that Davey/Priestley do not point out
  non-emptyness of the set @term{??H}, (which is obvious, but not
  vacous).
 
  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;
   assume mono: "mono f";