no longer delay loading of assoc_fold.ML
authorhuffman
Mon Mar 30 10:47:41 2009 -0700 (2009-03-30)
changeset 30796126701134811
parent 30794 787b39d499cf
child 30797 ef13967f911f
child 30802 f9e9e800d27e
no longer delay loading of assoc_fold.ML
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Mon Mar 30 17:14:44 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Mar 30 10:47:41 2009 -0700
     1.3 @@ -12,7 +12,7 @@
     1.4  uses
     1.5    ("Tools/numeral.ML")
     1.6    ("Tools/numeral_syntax.ML")
     1.7 -  ("~~/src/Provers/Arith/assoc_fold.ML")
     1.8 +  "~~/src/Provers/Arith/assoc_fold.ML"
     1.9    "~~/src/Provers/Arith/cancel_numerals.ML"
    1.10    "~~/src/Provers/Arith/combine_numerals.ML"
    1.11    ("Tools/int_arith.ML")
    1.12 @@ -1525,7 +1525,6 @@
    1.13  lemmas zle_int = of_nat_le_iff [where 'a=int]
    1.14  lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
    1.15  
    1.16 -use "~~/src/Provers/Arith/assoc_fold.ML"
    1.17  use "Tools/int_arith.ML"
    1.18  declaration {* K Int_Arith.setup *}
    1.19