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.
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.
This issue is still open. Who feels resonsible to fix it? Brian or
Andreas Lochbihler himself?
Gerwin normally allocates 1 or 2 weeks after an Isabelle release to
finalize stable AFP, but if the above requires further changes to Isabelle
than it is too late.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
