Hi again,
> 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
Update: The same problem occurs already with revision 6975db7fd6f0, i.e. it has
nothing to do with my recent changes to the "metis" proof method and is
apparently unrelated to the AFP failure. To reproduce it, fire up Proof General
with the HOL image and process
theory Scratch
imports Main
begin
lemma "a : {x. P x} ==> P a"
proof -
assume "a : {x. P x}"
hence "a : P" apply (metis Collect_def) done
The disturbing error message should appear on the "done".
When it comes to the AFP failure, there's a second AFP failure, in
JinjaThreads, that's obviously related to the servers' being down yesterday;
the Lam-ml-Normalization failure could be due to that, too. Lukas is helping
find out.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
