# HG changeset patch
# User paulson
# Date 966617162 -7200
# Node ID 9754ba005b646b173ac8bc4bf3b375f17e9b27bd
# Parent  2937a854e3d724baa648fa79370fdf234ca7ad74
X-symbols for ordinal, cardinal, integer arithmetic

diff -r 2937a854e3d7 -r 9754ba005b64 src/ZF/Arith.thy
--- 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
diff -r 2937a854e3d7 -r 9754ba005b64 src/ZF/CardinalArith.thy
--- 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
diff -r 2937a854e3d7 -r 9754ba005b64 src/ZF/Integ/Int.thy
--- 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
diff -r 2937a854e3d7 -r 9754ba005b64 src/ZF/OrderType.thy
--- 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