| changeset 21404 | eb85850d3eb7 |
| parent 21210 | c17fd2df4e9e |
| child 23315 | df3a7e9ebadb |
--- a/src/HOL/Library/Nat_Infinity.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Library/Nat_Infinity.thy Fri Nov 17 02:20:03 2006 +0100 @@ -28,7 +28,7 @@ instance inat :: "{ord, zero}" .. definition - iSuc :: "inat => inat" + iSuc :: "inat => inat" where "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)" defs (overloaded)