src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -10,10 +10,6 @@
 imports Inductive Typedef Fun Rings
 begin
 
-named_theorems arith "arith facts -- only ground formulas"
-ML_file "Tools/arith_data.ML"
-
-
 subsection \<open>Type \<open>ind\<close>\<close>
 
 typedecl ind