[isabelle-dev] AFP/JinjaThreads failure

Brian Huffman huffman at in.tum.de
Tue Apr 10 19:37:32 CEST 2012

On Tue, Apr 10, 2012 at 3:06 PM, Makarius <makarius at 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

I guess the quick fix would be to declare some extra code equations
manually. The proper fix would be to figure out exactly how and when
the lift_definition command should declare code equations

- Brian

More information about the isabelle-dev mailing list