src/HOL/Integ/IntArith.thy
author wenzelm
Wed, 08 May 2002 12:15:30 +0200
changeset 13122 c63612ffb186
parent 12023 d982f98e0f0d
child 13575 ecb6ecd9af13
permissions -rw-r--r--
oops;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12023
wenzelm
parents: 11868
diff changeset
     1
wenzelm
parents: 11868
diff changeset
     2
header {* Integer arithmetic *}
wenzelm
parents: 11868
diff changeset
     3
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     4
theory IntArith = Bin
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     5
files ("int_arith1.ML") ("int_arith2.ML"):
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     6
12023
wenzelm
parents: 11868
diff changeset
     7
use "int_arith1.ML"
wenzelm
parents: 11868
diff changeset
     8
setup int_arith_setup
wenzelm
parents: 11868
diff changeset
     9
use "int_arith2.ML"
wenzelm
parents: 11868
diff changeset
    10
declare zabs_split [arith_split]
wenzelm
parents: 11868
diff changeset
    11
7707
1f4b67fdfdae simprocs now in IntArith;
wenzelm
parents:
diff changeset
    12
end