Re: [isabelle] Theory name conflict

On Mon, 17 Jan 2011, Mathieu Giorgino wrote:

For example:

 theory Scratch
   imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"


 theory Scratch
   imports "/non/existing/path/Nat"

are prefectly fine even after a new pull (41597:ced4f78bb728), update, HOL make.

Yes, that's a "normal" feature of paths in theory imports.

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 is strange.  Can you try this all-inclusive version?

What is your OS, Proof General and Emacs version anyway?


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