[isabelle] "Clash of specification" error



Hi,

It seems I'm unable to use the Word_Enum theory from the AFP Word
library and List_lexord theory from the HOL Library concurrently as
Isabelle-2016 raises the following exception when processing
dependencies:

Clash of specifications for less:
  "List_lexord.ord_list_inst.less_list_def"â
  "Prefix_Order.ord_list_inst.less_list_def"â

Minimum example:

theory
  Error_Monad
imports
  Main
  "$AFP/Word_Lib/Word_Enum"
  "~~/src/HOL/Library/List_lexord"
begin

(* XXX *)

end


(In my development, I'm importing List_lexord in X.thy and Word_Enum
in Y.thy with a dependency between the two.)

Is there a way around this?

Thanks,
Dominic




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.