--- a/src/ZF/Cardinal.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Cardinal.thy Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
swap :: "[i,i,i]=>i" (*not used; useful??*)
-rules
+defs
(*least ordinal operator*)
Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"