Re: [isabelle] updating code that calls add_locale_i
On 11/02/10 11:39, Michael Norrish wrote:
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.
Actually, I see now that I can omit the term by using Named  or
Positional , which I guess is appropriate because I don't want to
pass any parameters to the one parent locale. But then, I still need to
provide two strings in the 'term expr, one of them coupled with a
boolean. The old code's globloc is a single string; and what of that boolean?
This archive was generated by a fusion of
Pipermail (Mailman edition) and