Re: [isabelle] Interpretations and lemmas



On 30 Oct 2006, at 7:06, Dr. Brendan Patrick Mahony wrote:

Is this a bug in the locale mechanism?

theory test = Main:

...

lemmas (in Double) z4 = z1 z2

this last fails with

*** Match
*** At command "lemmas".

Which version of Isabelle are you refering to? The exception is no longer present in the current repository version.

Clemens






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.