src/ZF/ex/Bin.thy
changeset 589 31847a7504ec
parent 515 abcc438e7c27
child 753 ec86863e87c8
equal deleted inserted replaced
588:91d5ac5ebb17 589:31847a7504ec
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 Arithmetic on binary integers.
     6 Arithmetic on binary integers.
     7 *)
     7 *)
     8 
     8 
     9 Bin = Integ + Univ + 
     9 Bin = Integ + Univ + "twos_compl" +
    10 consts
    10 consts
    11   bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
    11   bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
    12   integ_of_bin     :: "i=>i"
    12   integ_of_bin     :: "i=>i"
    13   bin_succ         :: "i=>i"
    13   bin_succ         :: "i=>i"
    14   bin_pred         :: "i=>i"
    14   bin_pred         :: "i=>i"