src/HOL/Integ/IntArith.thy
author wenzelm
Sat Nov 03 01:33:54 2001 +0100 (2001-11-03)
changeset 12023 d982f98e0f0d
parent 11868 56db9f3a6b3e
child 13575 ecb6ecd9af13
permissions -rw-r--r--
tuned;
wenzelm@12023
     1
wenzelm@12023
     2
header {* Integer arithmetic *}
wenzelm@12023
     3
wenzelm@9436
     4
theory IntArith = Bin
wenzelm@9436
     5
files ("int_arith1.ML") ("int_arith2.ML"):
wenzelm@9436
     6
wenzelm@12023
     7
use "int_arith1.ML"
wenzelm@12023
     8
setup int_arith_setup
wenzelm@12023
     9
use "int_arith2.ML"
wenzelm@12023
    10
declare zabs_split [arith_split]
wenzelm@12023
    11
wenzelm@7707
    12
end