src/HOL/Library/Nat_Infinity.thy

 
 instantiation inat :: comm_monoid_add
 begin
 
 definition
-  [code del]: "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
+  "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]:
   "Fin m + Fin n = Fin (m + n)"
   "\<infinity> + q = \<infinity>"
   "q + \<infinity> = \<infinity>"

 
 instantiation inat :: comm_semiring_1
 begin
 
 definition
-  times_inat_def [code del]:
+  times_inat_def:
   "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)))"
 
 lemma times_inat_simps [simp, code]:
   "Fin m * Fin n = Fin (m * n)"

 
 instantiation inat :: linordered_ab_semigroup_add
 begin
 
 definition
-  [code del]: "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
+  "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
-  [code del]: "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
+  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
     | \<infinity> \<Rightarrow> False)"
 
 lemma inat_ord_simps [simp]:
   "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   "Fin m < Fin n \<longleftrightarrow> m < n"