On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein <[email protected]> wrote: > 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?
This must be due to the recent changeset: added syntactic classes for "inf" and "sup" http://isabelle.in.tum.de/repos/isabelle/rev/5e51075cbd97 The fix is probably to replace "semilattice_sup_class.sup" with "sup_class.sup". - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
