Hi all,
Somewhere between 43ca06e6c168 and 6975db7fd6f0, I seem to have broken the AFP
entry "Lam-ml-Normalization". However, I cannot reproduce the problem on my
machine -- whether in Proof General nor using "isabelle make".
On the other hand, I do get the following disturbing messages in Proof General:
Exception trace for exception - UNDEF raised in Isar/toplevel.ML line 494
Toplevel.end_proof(1)(1)(1)
End of trace
Exception trace for exception - UNDEF raised in Isar/toplevel.ML line 457
Toplevel.end_local_theory-(1)(1)
End of trace
If anybody has a clue about what's going on, please say so. In any case, I will
continue investigating.
Thanks,
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
