src/HOL/Nat.thy
changeset 57952 1a9a6dfc255f
parent 57514 bdc2c6b40bf2
child 57983 6edc3529bb4e
     1.1 --- a/src/HOL/Nat.thy	Sat Aug 16 14:27:41 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Aug 16 14:32:26 2014 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4  begin
     1.5  
     1.6  ML_file "~~/src/Tools/rat.ML"
     1.7 +
     1.8 +named_theorems arith "arith facts -- only ground formulas"
     1.9  ML_file "Tools/arith_data.ML"
    1.10  ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.11