src/HOL/Integ/IntArith.thy
author wenzelm
Fri, 10 Nov 2000 19:03:55 +0100
changeset 10434 6ea4735c3955
parent 9436 62bb04ab4b01
child 10574 8f98f0301d67
permissions -rw-r--r--
simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     1
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     2
theory IntArith = Bin
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     3
files ("int_arith1.ML") ("int_arith2.ML"):
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     4
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     5
use "int_arith1.ML"	setup int_arith_setup
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     6
use "int_arith2.ML"	lemmas [arith_split] = zabs_split
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     7
7707
1f4b67fdfdae simprocs now in IntArith;
wenzelm
parents:
diff changeset
     8
end