[isabelle-dev] sets and code generation

[Florian Haftmann]

Hi Jesus,

> trying to import simultaneously the theory file
> "HOL/Matrix/Matrix.thy" and the afp entry
> http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems
> that the second theory file "unloads" the first one (as Makarius
> suggested in his mail):
> 
> theory Matrix_ex
>   imports
>   "~~/src/HOL/Matrix/Matrix"
>   "Matrix/Matrix"
> begin
> 
> Is there an easy way out of this situation in Isabelle2011-1? Renaming
> one of the theory files is an acceptable solution in this case?

It is.  Cf. the previous email of Makarius on the same thread.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120328/92a17d45/attachment.sig>