[isabelle-dev] Fwd: status (AFP)

Brian Huffman brianh at cs.pdx.edu
Sun Sep 18 14:40:29 CEST 2011

On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein <gerwin.klein at nicta.com.au> 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"

The fix is probably to replace "semilattice_sup_class.sup" with "sup_class.sup".

- Brian

More information about the isabelle-dev mailing list