| changeset 30729 | 461ee3e49ad3 |
| parent 30198 | 922f944f03b2 |
| child 30968 | 10fef94f40fc |
--- a/src/HOL/NSA/StarDef.thy Thu Mar 26 19:24:21 2009 +0100 +++ b/src/HOL/NSA/StarDef.thy Thu Mar 26 20:08:55 2009 +0100 @@ -23,7 +23,7 @@ apply (rule nat_infinite) done -interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat +interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat by (rule freeultrafilter_FreeUltrafilterNat) text {* This rule takes the place of the old ultra tactic *}