equal
deleted
inserted
replaced
184 |
184 |
185 |
185 |
186 subsection{*Nonstandard Characterization of Induction*} |
186 subsection{*Nonstandard Characterization of Induction*} |
187 |
187 |
188 definition |
188 definition |
189 hSuc :: "hypnat => hypnat" |
189 hSuc :: "hypnat => hypnat" where |
190 "hSuc n = n + 1" |
190 "hSuc n = n + 1" |
191 |
191 |
192 lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)" |
192 lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)" |
193 by (rule starP_star_n) |
193 by (rule starP_star_n) |
194 |
194 |