| changeset 21404 | eb85850d3eb7 |
| parent 20740 | 5a103b43da5a |
| child 21847 | 59a68ed9f2f2 |
--- a/src/HOL/Hyperreal/NatStar.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Hyperreal/NatStar.thy Fri Nov 17 02:20:03 2006 +0100 @@ -186,7 +186,7 @@ subsection{*Nonstandard Characterization of Induction*} definition - hSuc :: "hypnat => hypnat" + hSuc :: "hypnat => hypnat" where "hSuc n = n + 1" lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"