[isabelle-dev] sets and code generation
florian.haftmann at informatik.tu-muenchen.de
Wed Mar 28 20:58:55 CEST 2012
> 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
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev