Re: [isabelle] Theory name conflict



But

   theory Scratch
   imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
     "$PATH_TO_AFP/Collections/common/Array"
   begin

on its own works – not that I would call that a well-defined behaviour.

When I try it, it loads Imperative_HOL, but nothing from Collections.

Alex





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