load Tools/numeral.ML in Num.thy
authorhuffman
Fri Mar 30 16:44:23 2012 +0200 (2012-03-30)
changeset 472284f4d85c3516f
parent 47227 bc18fa07053b
child 47229 ba37aaead155
load Tools/numeral.ML in Num.thy
src/HOL/Int.thy
src/HOL/Num.thy
     1.1 --- a/src/HOL/Int.thy	Fri Mar 30 16:43:07 2012 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri Mar 30 16:44:23 2012 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  theory Int
     1.5  imports Equiv_Relations Wellfounded
     1.6  uses
     1.7 -  ("Tools/numeral.ML")
     1.8    ("Tools/int_arith.ML")
     1.9  begin
    1.10  
    1.11 @@ -835,7 +834,6 @@
    1.12    of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.13    of_int_0 of_int_1 of_int_add of_int_mult
    1.14  
    1.15 -use "Tools/numeral.ML"
    1.16  use "Tools/int_arith.ML"
    1.17  declaration {* K Int_Arith.setup *}
    1.18  
     2.1 --- a/src/HOL/Num.thy	Fri Mar 30 16:43:07 2012 +0200
     2.2 +++ b/src/HOL/Num.thy	Fri Mar 30 16:44:23 2012 +0200
     2.3 @@ -7,6 +7,8 @@
     2.4  
     2.5  theory Num
     2.6  imports Datatype
     2.7 +uses
     2.8 +  ("Tools/numeral.ML")
     2.9  begin
    2.10  
    2.11  subsection {* The @{text num} type *}
    2.12 @@ -331,6 +333,9 @@
    2.13      (@{const_syntax neg_numeral}, num_tr' "-")] end
    2.14  *}
    2.15  
    2.16 +use "Tools/numeral.ML"
    2.17 +
    2.18 +
    2.19  subsection {* Class-specific numeral rules *}
    2.20  
    2.21  text {*