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
