src/ZF/OrderType.thy

--- a/src/ZF/OrderType.thy	Thu Apr 13 11:32:44 1995 +0200
+++ b/src/ZF/OrderType.thy	Thu Apr 13 11:33:57 1995 +0200
@@ -17,6 +17,7 @@
 
   "**"      :: "[i,i]=>i"           (infixl 70)
   "++"      :: "[i,i]=>i"           (infixl 65)
+  "--"      :: "[i,i]=>i"           (infixl 65)
  
 
 defs
@@ -34,4 +35,7 @@
   (*ordinal addition*)
   oadd_def      "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
 
+  (*ordinal subtraction*)
+  odiff_def     "i -- j == ordertype(i-j, Memrel(i))"
+
 end