changeset 47228 | 4f4d85c3516f |
parent 47226 | ea712316fc87 |
child 47255 | 30a1692557b0 |
--- a/src/HOL/Int.thy Fri Mar 30 16:43:07 2012 +0200 +++ b/src/HOL/Int.thy Fri Mar 30 16:44:23 2012 +0200 @@ -8,7 +8,6 @@ theory Int imports Equiv_Relations Wellfounded uses - ("Tools/numeral.ML") ("Tools/int_arith.ML") begin @@ -835,7 +834,6 @@ of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult of_int_0 of_int_1 of_int_add of_int_mult -use "Tools/numeral.ML" use "Tools/int_arith.ML" declaration {* K Int_Arith.setup *}