--- a/src/ZF/Arith.thy Fri Aug 18 18:11:10 2000 +0200
+++ b/src/ZF/Arith.thy Fri Aug 18 18:46:02 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/arith.thy
+(* Title: ZF/Arith.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
@@ -56,4 +56,7 @@
mod :: [i,i]=>i (infixl "mod" 70)
"m mod n == raw_mod (natify(m), natify(n))"
+syntax (symbols)
+ "mult" :: [i, i] => i (infixr "#\\<times>" 70)
+
end
--- a/src/ZF/CardinalArith.thy Fri Aug 18 18:11:10 2000 +0200
+++ b/src/ZF/CardinalArith.thy Fri Aug 18 18:46:02 2000 +0200
@@ -39,4 +39,7 @@
(*needed because jump_cardinal(K) might not be the successor of K*)
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
+syntax (symbols)
+ "op |*|" :: [i,i] => i (infixr "|\\<times>|" 70)
+
end
--- a/src/ZF/Integ/Int.thy Fri Aug 18 18:11:10 2000 +0200
+++ b/src/ZF/Integ/Int.thy Fri Aug 18 18:46:02 2000 +0200
@@ -67,4 +67,9 @@
zle :: [i,i]=>o (infixl "$<=" 50)
"z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
+
+syntax (symbols)
+ "zmult" :: [i,i] => i (infixr "$\\<times>" 70)
+ "zle" :: [i,i] => o (infixl "$\\<le>" 50) (*less than or equals*)
+
end
--- a/src/ZF/OrderType.thy Fri Aug 18 18:11:10 2000 +0200
+++ b/src/ZF/OrderType.thy Fri Aug 18 18:46:02 2000 +0200
@@ -38,4 +38,7 @@
(*ordinal subtraction*)
odiff_def "i -- j == ordertype(i-j, Memrel(i))"
+syntax (symbols)
+ "op **" :: [i,i] => i (infixr "\\<times>\\<times>" 70)
+
end