[isabelle-dev] Fwd: status (AFP)

Gerwin Klein gerwin.klein at nicta.com.au
Sun Sep 18 10:42:08 CEST 2011

After not running in the test for quite some time, JinjaThreads now comes back failing:

*** Undeclared constant: "semilattice_sup_class.sup"
*** At command "definition" (line 20 of "/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
val it = (): unit
Exception- TOPLEVEL_ERROR raised
*** ML error

It looks like something in the class setup changed slightly. Could somebody who is more up-to-date in this area have a look, please?

For the Isabelle release, we need to have all AFP entries in working order.


More information about the isabelle-dev mailing list