--- a/src/HOL/Library/Nat_Infinity.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Sat May 27 17:42:02 2006 +0200
@@ -19,20 +19,20 @@
datatype inat = Fin nat | Infty
+const_syntax (xsymbols)
+ Infty ("\<infinity>")
+
+const_syntax (HTML output)
+ Infty ("\<infinity>")
+
instance inat :: "{ord, zero}" ..
-consts
+definition
iSuc :: "inat => inat"
-
-syntax (xsymbols)
- Infty :: inat ("\<infinity>")
+ "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
-syntax (HTML output)
- Infty :: inat ("\<infinity>")
-
-defs
+defs (overloaded)
Zero_inat_def: "0 == Fin 0"
- iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>"
iless_def: "m < n ==
case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
| \<infinity> => False"
@@ -114,7 +114,6 @@
by (simp add: inat_defs split:inat_splits, arith?)
-(* ----------------------------------------------------------------------- *)
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
by (simp add: inat_defs split:inat_splits, arith?)