author | lcp |
Thu, 13 Apr 1995 11:33:57 +0200 | |
changeset 1033 | 437728256de3 |
parent 1032 | 54b9f670c67e |
child 1034 | ccc9a3cbca05 |
--- 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