On Thu, 19 Apr 2012, Brian Huffman wrote:
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.
Thanks. It works on lxbroy10:
T
On Thu, Apr 19, 2012 at 4:02 PM, Makarius wrote:
> On Tue, 10 Apr 2012, Brian Huffman wrote:
>
>> On Tue, Apr 10, 2012 at 3:06 PM, Makarius wrote:
>>>
>>> Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
>>>
>>> *** No code equations for one_word_inst.one_word
>>> *** At co
On Tue, 10 Apr 2012, Brian Huffman wrote:
On Tue, Apr 10, 2012 at 3:06 PM, Makarius 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")
On Tue, Apr 10, 2012 at 3:06 PM, Makarius 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
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?
Makarius
__
