src/ZF/arith.thy
changeset 124 858ab9a9b047
parent 25 3ac1c0c0016e
equal deleted inserted replaced
123:0a2f744e008a 124:858ab9a9b047
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Arithmetic operators and their definitions
     6 Arithmetic operators and their definitions
     7 *)
     7 *)
     8 
     8 
     9 Arith = Epsilon +
     9 Arith = Epsilon + "simpdata" +
    10 consts
    10 consts
    11     rec  :: "[i, i, [i,i]=>i]=>i"
    11     rec  :: "[i, i, [i,i]=>i]=>i"
    12     "#*" :: "[i,i]=>i"      		(infixl 70)
    12     "#*" :: "[i,i]=>i"      		(infixl 70)
    13     div  :: "[i,i]=>i"      		(infixl 70) 
    13     div  :: "[i,i]=>i"      		(infixl 70) 
    14     mod  :: "[i,i]=>i"      		(infixl 70)
    14     mod  :: "[i,i]=>i"      		(infixl 70)