| changeset 54580 | 7b9336176a1c |
| parent 54489 | 03ff4d1e6784 |
| child 55911 | d00023bd3554 |
--- a/src/HOL/NSA/StarDef.thy Mon Nov 25 10:20:25 2013 +0100 +++ b/src/HOL/NSA/StarDef.thy Mon Nov 25 12:27:03 2013 +0100 @@ -18,7 +18,7 @@ apply (unfold FreeUltrafilterNat_def) apply (rule someI_ex) apply (rule freeultrafilter_Ex) -apply (rule nat_infinite) +apply (rule infinite_UNIV_nat) done interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat