On Thu, Apr 19, 2012 at 4:02 PM, Makarius <makar...@sketis.net> wrote: > On Tue, 10 Apr 2012, Brian Huffman wrote: > >> On Tue, Apr 10, 2012 at 3:06 PM, Makarius <makar...@sketis.net> wrote: >>> >>> Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error: >>> >>> *** No code equations for one_word_inst.one_word >>> *** At command "by" (line 174 of >>> "afp-devel/thys/JinjaThreads/Common/BinOp.thy") >>> >>> What needs to be done here? >> >> >> This is probably related to my changeset Isabelle/9475d524bafb, where >> I redefined a bunch of word operations with lift_definition instead of >> definition.
Hopefully changeset e3c699a1fae6 will take care of the problem. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev