diff -r 80edb859fd24 -r b9e14471629c src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Wed Aug 21 15:57:08 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Wed Aug 21 15:57:24 2002 +0200
@@ -42,7 +42,7 @@
                  --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
 
   wellordered :: "[i=>o,i,i]=>o"
-    --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
+    --{*linear and wellfounded on @{text A}*}
     "wellordered(M,A,r) == 
 	transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"