src/HOL/Library/Nat_Infinity.thy
changeset 11701 3d51fbf81c17
parent 11655 923e4d0d36d5
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -31,14 +31,14 @@
     1.4    Infty :: inat    ("\<infinity>")
     1.5  
     1.6  defs
     1.7 -  iZero_def: "0 == Fin 0"
     1.8 +  Zero_inat_def: "0 == Fin 0"
     1.9    iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    1.10    iless_def: "m < n ==
    1.11      case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
    1.12      | \<infinity>  => False"
    1.13    ile_def: "(m::inat) \<le> n == \<not> (n < m)"
    1.14  
    1.15 -lemmas inat_defs = iZero_def iSuc_def iless_def ile_def
    1.16 +lemmas inat_defs = Zero_inat_def iSuc_def iless_def ile_def
    1.17  lemmas inat_splits = inat.split inat.split_asm
    1.18  
    1.19  text {*