Re: [isabelle-dev] sets and code generation
On Tue, 27 Mar 2012, Jesus Aransay wrote: 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 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? Renaming one of the theory files (on your private copy) is the only solution in contemporary Isabelle. It is acceptable, because it is just one file here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isatest
On Thu, 29 Mar 2012, Gerwin Klein wrote: On 29/03/2012, at 6:11 AM, Makarius wrote: Who is the main responsible for isatest anyway? According to the received customs it would be Gerwin, since he started the service many years ago. (His shell scripts still mention SunOS.) I still feel mildly responsible for isatest, but would be more than happy to pass this on to somebody with more time and more close in time(zone) and and space to where it actually runs. To summarize this mail thread for permanence in the mail archive: We keep the status-quo, i.e. Gerwin is historically responsible for isatest, but I keep it running in everyday business. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] AFP/JinjaThreads failure
Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error: *** No code equations for one_word_inst.one_word *** At command by (line 174 of afp-devel/thys/JinjaThreads/Common/BinOp.thy) What needs to be done here? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
