src/HOL/Nat.thy
changeset 30686 47a32dd1b86e
parent 30496 7cdcc9dd95cb
child 30954 cf50e67bc1d1
     1.1 --- a/src/HOL/Nat.thy	Mon Mar 23 19:01:15 2009 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Mar 23 19:01:16 2009 +0100
     1.3 @@ -63,9 +63,8 @@
     1.4  end
     1.5  
     1.6  lemma Suc_not_Zero: "Suc m \<noteq> 0"
     1.7 -  apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
     1.8 +  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
     1.9      Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
    1.10 -  done
    1.11  
    1.12  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    1.13    by (rule not_sym, rule Suc_not_Zero not_sym)
    1.14 @@ -82,7 +81,7 @@
    1.15    done
    1.16  
    1.17  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.18 -  -- {* for backward compatibility -- naming of variables differs *}
    1.19 +  -- {* for backward compatibility -- names of variables differ *}
    1.20    fixes n
    1.21    assumes "P 0"
    1.22      and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.23 @@ -1345,19 +1344,13 @@
    1.24    shows "u = s"
    1.25    using 2 1 by (rule trans)
    1.26  
    1.27 +setup Arith_Data.setup
    1.28 +
    1.29  use "Tools/nat_arith.ML"
    1.30  declaration {* K Nat_Arith.setup *}
    1.31  
    1.32 -ML{*
    1.33 -structure ArithFacts =
    1.34 -  NamedThmsFun(val name = "arith"
    1.35 -               val description = "arith facts - only ground formulas");
    1.36 -*}
    1.37 -
    1.38 -setup ArithFacts.setup
    1.39 -
    1.40  use "Tools/lin_arith.ML"
    1.41 -declaration {* K LinArith.setup *}
    1.42 +declaration {* K Lin_Arith.setup *}
    1.43  
    1.44  lemmas [arith_split] = nat_diff_split split_min split_max
    1.45