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.