--- a/src/ZF/AC/WO1_WO7.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO1_WO7.ML Mon May 21 14:45:52 2001 +0200
@@ -31,7 +31,7 @@
(* ********************************************************************** *)
(* The Rubins' proof of the other implication is contained within the *)
-(* following sentence : *)
+(* following sentence \\<in> *)
(* "... each infinite ordinal is well ordered by < but not by >." *)
(* This statement can be proved by the following two theorems. *)
(* But moreover we need to show similar property for any well ordered *)