Re: [isabelle] Theory name conflict



On Mon, 17 Jan 2011, Mathieu Giorgino wrote:

For example:

 theory Scratch
   imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
   "/non/existing/path/Array"
 begin

and

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

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?

  http://www4.in.tum.de/~wenzelm/test/Isabelle_14-Jan-2011/download.html


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


	Makarius





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