| changeset 9436 | 62bb04ab4b01 |
| parent 9214 | 9454f30eacc7 |
| child 10574 | 8f98f0301d67 |
--- a/src/HOL/Integ/IntArith.thy Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/IntArith.thy Tue Jul 25 00:06:46 2000 +0200 @@ -1,2 +1,8 @@ -theory IntArith = Bin: + +theory IntArith = Bin +files ("int_arith1.ML") ("int_arith2.ML"): + +use "int_arith1.ML" setup int_arith_setup +use "int_arith2.ML" lemmas [arith_split] = zabs_split + end