src/ZF/ord.thy
changeset 30 d49df4181f0d
parent 0 a5a9c433f639
child 124 858ab9a9b047
--- a/src/ZF/ord.thy	Tue Oct 05 17:49:23 1993 +0100
+++ b/src/ZF/ord.thy	Wed Oct 06 09:58:53 1993 +0100
@@ -1,19 +1,25 @@
 (*  Title: 	ZF/ordinal.thy
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    Copyright   1993  University of Cambridge
 
 Ordinals in Zermelo-Fraenkel Set Theory 
 *)
 
 Ord = WF +
 consts
-    Memrel      	::      "i=>i"
-    Transset,Ord        ::      "i=>o"
+  Memrel      	:: "i=>i"
+  Transset,Ord  :: "i=>o"
+  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
+  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
+
+translations
+  "x le y"      == "x < succ(y)"
 
 rules
   Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   Transset_def	"Transset(i) == ALL x:i. x<=i"
   Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
+  lt_def        "i<j         == i:j & Ord(j)"
 
 end