changeset 64438 | f91cae6c1d74 |
parent 64435 | c93b0e6131c3 |
child 64600 | 86e2f2208a58 |
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Nov 01 00:55:52 2016 +0100 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Nov 01 01:04:53 2016 +0100 @@ -20,7 +20,7 @@ apply (rule infinite_UNIV_nat) done -interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat +interpretation FreeUltrafilterNat: freeultrafilter \<U> by (rule freeultrafilter_FreeUltrafilterNat)