[isabelle-dev] sets and code generation

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Mar 28 20:58:55 CEST 2012

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.



PGP available:

-------------- 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>

More information about the isabelle-dev mailing list