Re: [isabelle] Theory name conflict
Le lundi 17 janvier 2011 07:54:19, Florian Haftmann a écrit :
> >> 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.
> > This looks strange, and should not import two different "Array"
> > theories. Which Isabelle version is this actually?
> I am not able to reproduce this behaviour. Maybe it was just an
> accidental situation while interactively changing the imports over and
I have tried this again and it worked... even when I discovered an error in my
path to the afp... which is silently ignored by Isabelle. In fact, putting any
path finishing with a theory name already existing in other imports, is
are prefectly fine even after a new pull (41597:ced4f78bb728), update, HOL
Furthermore, I am still able to import two theories with the same name (after
a check of the paths, and a "fresh" isabelle emacs)... and I can't see/imagine
the difference with your configurations...
This archive was generated by a fusion of
Pipermail (Mailman edition) and