src/HOL/Library/Nat_Infinity.thy
changeset 19736 d8d0f8f51d69
parent 15140 322485b816ac
child 21210 c17fd2df4e9e
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -19,20 +19,20 @@
     1.4  
     1.5  datatype inat = Fin nat | Infty
     1.6  
     1.7 +const_syntax (xsymbols)
     1.8 +  Infty  ("\<infinity>")
     1.9 +
    1.10 +const_syntax (HTML output)
    1.11 +  Infty  ("\<infinity>")
    1.12 +
    1.13  instance inat :: "{ord, zero}" ..
    1.14  
    1.15 -consts
    1.16 +definition
    1.17    iSuc :: "inat => inat"
    1.18 -
    1.19 -syntax (xsymbols)
    1.20 -  Infty :: inat    ("\<infinity>")
    1.21 +  "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
    1.22  
    1.23 -syntax (HTML output)
    1.24 -  Infty :: inat    ("\<infinity>")
    1.25 -
    1.26 -defs
    1.27 +defs (overloaded)
    1.28    Zero_inat_def: "0 == Fin 0"
    1.29 -  iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    1.30    iless_def: "m < n ==
    1.31      case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
    1.32      | \<infinity>  => False"
    1.33 @@ -114,7 +114,6 @@
    1.34    by (simp add: inat_defs split:inat_splits, arith?)
    1.35  
    1.36  
    1.37 -(* ----------------------------------------------------------------------- *)
    1.38  
    1.39  lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
    1.40    by (simp add: inat_defs split:inat_splits, arith?)