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