# HG changeset patch
# User blanchet
# Date 1280767971 -7200
# Node ID ab528533db92eff6256e21fc04e2f6a007abf998
# Parent  28bb89672cc7303a48fb3652ae84ecfd968dbea8
help Nitpick

diff -r 28bb89672cc7 -r ab528533db92 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Aug 02 18:39:14 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 02 18:52:51 2010 +0200
@@ -125,7 +125,7 @@
 instantiation inat :: comm_monoid_add
 begin
 
-definition
+definition [nitpick_simp]:
   "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
 
 lemma plus_inat_simps [simp, code]:
@@ -176,8 +176,7 @@
 instantiation inat :: comm_semiring_1
 begin
 
-definition
-  times_inat_def:
+definition times_inat_def [nitpick_simp]:
   "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
     (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
 
@@ -237,11 +236,11 @@
 instantiation inat :: linordered_ab_semigroup_add
 begin
 
-definition
+definition [nitpick_simp]:
   "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
     | \<infinity> \<Rightarrow> True)"
 
-definition
+definition [nitpick_simp]:
   "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
     | \<infinity> \<Rightarrow> False)"