Re: [isabelle] Problems with Char_ord
Am 25/08/2012 16:43, schrieb Brian Huffman:
> On Fri, Aug 24, 2012 at 12:56 PM, Manuel Eberl <eberlm at in.tum.de> wrote:
>> I need a linorder on strings and imported List_lexord and Char_ord for
>> that purpose. However, when Isabelle tries to process the imports
>> command, I get the following error:
>> Clash of specifications "Misc.ord_prod_inst.less_prod_def" and
>> "Product_ord.ord_prod_inst.less_prod_def" for constant
>> I suspect that this has something to do with conflicting definitions of
>> product orderings. The first one seems to come from
>> Library/Product_ord.thy The second one probably comes from some kind of
>> file that is imported by the Collection framework, which I use - perhaps
>> Collections/common/Misc.thy. But how do I fix this?
> Library/Char_ord.thy imports Library/Product_ord.thy, but upon
> inspection it looks like this dependency is completely unnecessary. So
> probably the easiest workaround is to modify Char_ord.thy by removing
> "Product_ord" from the imports.
> Someone ought to make this change in the repository version as well.
> - Brian
This archive was generated by a fusion of
Pipermail (Mailman edition) and