src/HOL/Nat.thy
changeset 66810 cc2b490f9dc4
parent 66386 962c12353c67
child 66816 212a3334e7da
     1.1 --- a/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -10,10 +10,6 @@
     1.4  imports Inductive Typedef Fun Rings
     1.5  begin
     1.6  
     1.7 -named_theorems arith "arith facts -- only ground formulas"
     1.8 -ML_file "Tools/arith_data.ML"
     1.9 -
    1.10 -
    1.11  subsection \<open>Type \<open>ind\<close>\<close>
    1.12  
    1.13  typedecl ind