I fixed the proof in JinjaThreads with changeset 78eb9266adb0.
However, due to the deeper reason that the classical reasoner setup has
been changed so that the original proof failed, one might have to look
into this specific subgoal again (understanding how the classical
reasoner has been changed).
(I am guessing it is due to the Predicate/Relation intro/elim changes.)
Lukas
On 03/19/2012 01:53 PM, Makarius wrote:
Dear all,
as of Isabelle/1d8601c642cc and AFP/039e21d114f1 the situation with
JinjaThreads is better than it used to be, but it still fails. The
critical bit is here:
*** Failed to finish proof
*** At command "by" (line 1123 of
"thys/JinjaThreads/Execute/Scheduler.thy")
It looks like a casualty of recent changes with 'a set, lattice,
inductive_set, numerals or similar.
This part of the session can be checked easily with only 2 cores and a
few GB of memory. So maybe someone who feels responsible for recent
changes in main HOL could take a look at it.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
