src/HOL/Nat.thy
changeset 48891 c0eafbd55de3
parent 48560 e0875d956a6b
child 49388 1ffd5a055acf
     1.1 --- a/src/HOL/Nat.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -9,14 +9,13 @@
     1.4  
     1.5  theory Nat
     1.6  imports Inductive Typedef Fun Fields
     1.7 -uses
     1.8 -  "~~/src/Tools/rat.ML"
     1.9 -  "Tools/arith_data.ML"
    1.10 -  ("Tools/nat_arith.ML")
    1.11 -  "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.12 -  ("Tools/lin_arith.ML")
    1.13  begin
    1.14  
    1.15 +ML_file "~~/src/Tools/rat.ML"
    1.16 +ML_file "Tools/arith_data.ML"
    1.17 +ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.18 +
    1.19 +
    1.20  subsection {* Type @{text ind} *}
    1.21  
    1.22  typedecl ind
    1.23 @@ -1492,7 +1491,7 @@
    1.24  
    1.25  setup Arith_Data.setup
    1.26  
    1.27 -use "Tools/nat_arith.ML"
    1.28 +ML_file "Tools/nat_arith.ML"
    1.29  
    1.30  simproc_setup nateq_cancel_sums
    1.31    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    1.32 @@ -1510,7 +1509,7 @@
    1.33    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
    1.34    {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
    1.35  
    1.36 -use "Tools/lin_arith.ML"
    1.37 +ML_file "Tools/lin_arith.ML"
    1.38  setup {* Lin_Arith.global_setup *}
    1.39  declaration {* K Lin_Arith.setup *}
    1.40