[isabelle] updating code that calls add_locale_i
My old code included:
Locale.add_locale_i (SOME "")
What should I do now that the nearest equivalent seems to be
Expression.add_locale? The type of the latter is a bit confusing. In
particular, the equivalent of the (Locale.Locale globloc) looks as if
it should be a expression_i, but such expressions have to include a
term if they are to convey any useful information at all, and it's
unclear to me quite what that term should be.
Or is Expression.add_locale not the right thing to be calling?
This archive was generated by a fusion of
Pipermail (Mailman edition) and