On Tue, Apr 10, 2012 at 3:06 PM, Makarius <[email protected]> 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. 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 automatically. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
