tuned
authorhaftmann
Thu Sep 30 08:50:45 2010 +0200 (2010-09-30)
changeset 397934bd217def154
parent 39792 4b615e3ddef7
child 39794 51451d73c3d4
tuned
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Thu Sep 30 07:34:06 2010 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Sep 30 08:50:45 2010 +0200
     1.3 @@ -149,11 +149,10 @@
     1.4  
     1.5  primrec minus_nat
     1.6  where
     1.7 -  diff_0:     "m - 0 = (m\<Colon>nat)"
     1.8 -  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
     1.9 +  diff_0 [code]: "m - 0 = (m\<Colon>nat)"
    1.10 +| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.11  
    1.12  declare diff_Suc [simp del]
    1.13 -declare diff_0 [code]
    1.14  
    1.15  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
    1.16    by (induct n) (simp_all add: diff_Suc)