X-symbols for ordinal, cardinal, integer arithmetic
authorpaulson
Fri Aug 18 18:46:02 2000 +0200 (2000-08-18)
changeset 96549754ba005b64
parent 9653 2937a854e3d7
child 9655 a4d2da014ec3
X-symbols for ordinal, cardinal, integer arithmetic
src/ZF/Arith.thy
src/ZF/CardinalArith.thy
src/ZF/Integ/Int.thy
src/ZF/OrderType.thy
     1.1 --- a/src/ZF/Arith.thy	Fri Aug 18 18:11:10 2000 +0200
     1.2 +++ b/src/ZF/Arith.thy	Fri Aug 18 18:46:02 2000 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      ZF/arith.thy
     1.5 +(*  Title:      ZF/Arith.thy
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1992  University of Cambridge
     1.9 @@ -56,4 +56,7 @@
    1.10    mod  :: [i,i]=>i                    (infixl "mod" 70)
    1.11      "m mod n == raw_mod (natify(m), natify(n))"
    1.12  
    1.13 +syntax (symbols)
    1.14 +  "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    1.15 +
    1.16  end
     2.1 --- a/src/ZF/CardinalArith.thy	Fri Aug 18 18:11:10 2000 +0200
     2.2 +++ b/src/ZF/CardinalArith.thy	Fri Aug 18 18:46:02 2000 +0200
     2.3 @@ -39,4 +39,7 @@
     2.4    (*needed because jump_cardinal(K) might not be the successor of K*)
     2.5    csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
     2.6  
     2.7 +syntax (symbols)
     2.8 +  "op |*|"     :: [i,i] => i          (infixr "|\\<times>|" 70)
     2.9 +
    2.10  end
     3.1 --- a/src/ZF/Integ/Int.thy	Fri Aug 18 18:11:10 2000 +0200
     3.2 +++ b/src/ZF/Integ/Int.thy	Fri Aug 18 18:46:02 2000 +0200
     3.3 @@ -67,4 +67,9 @@
     3.4    zle          ::      [i,i]=>o      (infixl "$<=" 50)
     3.5       "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
     3.6    
     3.7 +
     3.8 +syntax (symbols)
     3.9 +  "zmult"     :: [i,i] => i          (infixr "$\\<times>" 70)
    3.10 +  "zle"       :: [i,i] => o          (infixl "$\\<le>" 50)  (*less than or equals*)
    3.11 +
    3.12  end
     4.1 --- a/src/ZF/OrderType.thy	Fri Aug 18 18:11:10 2000 +0200
     4.2 +++ b/src/ZF/OrderType.thy	Fri Aug 18 18:46:02 2000 +0200
     4.3 @@ -38,4 +38,7 @@
     4.4    (*ordinal subtraction*)
     4.5    odiff_def     "i -- j == ordertype(i-j, Memrel(i))"
     4.6  
     4.7 +syntax (symbols)
     4.8 +  "op **"     :: [i,i] => i          (infixr "\\<times>\\<times>" 70)
     4.9 +
    4.10  end