Hi David, this looks like a bug. Which precise version of Isabelle are you using? Clemens On 10 Sep 2008, at 0:12, David Streader wrote:
I am lost as to what is wrong! The last lemma (see below or attached for simplified theory) results in error:*** exception Option raised *** At command "lemma".