Hi Lucas, Nice failure :-)
datatype Ta = C_2 "nat" "nat" | C_1 "Ta" "nat" fun f where "f (C_2 a b) c = c" | "f (C_1 a b) c = f a (f a (f a (f (C_1 a b) b)))" (* ... after a long time... constants f :: "Ta ⇒ nat ⇒ nat" Exception. At command "fun". *)
This is the termination prover looping. It keeps applying the psimp-rules, which are still in the simpset in Isabelle2009-2.
I took them out in 150f831ce4a3 since they caused other confusion, so it is no longer a problem in the next release. Now you can work around it by taking them out yourself.
I am not sure about the exception. It could be some "physical" interrupt due to hitting some ressource bound, which aborts the whole toplevel transaction, so you cannot handle it. But I am just guessing.
Alex _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
