1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Aug 02 18:39:14 2010 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 02 18:52:51 2010 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  instantiation inat :: comm_monoid_add
     1.5  begin
     1.6  
     1.7 -definition
     1.8 +definition [nitpick_simp]:
     1.9    "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
    1.10  
    1.11  lemma plus_inat_simps [simp, code]:
    1.12 @@ -176,8 +176,7 @@
    1.13  instantiation inat :: comm_semiring_1
    1.14  begin
    1.15  
    1.16 -definition
    1.17 -  times_inat_def:
    1.18 +definition times_inat_def [nitpick_simp]:
    1.19    "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
    1.20      (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
    1.21  
    1.22 @@ -237,11 +236,11 @@
    1.23  instantiation inat :: linordered_ab_semigroup_add
    1.24  begin
    1.25  
    1.26 -definition
    1.27 +definition [nitpick_simp]:
    1.28    "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
    1.29      | \<infinity> \<Rightarrow> True)"
    1.30  
    1.31 -definition
    1.32 +definition [nitpick_simp]:
    1.33    "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
    1.34      | \<infinity> \<Rightarrow> False)"
    1.35