Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]
Hi Clemens, > I didn't have time to look at your patches, and since I only have superficial knowledge of instantiation contexts I didn't fully understand the example either. I guess though that the purpose of these global interpretations is to propagate some constant declarations into the surrounding theory. If this is useful we should certainly have such a command. thanks for looking into that. > What I still fail to understand is why you want to use 'global_interpretation' as keyword if the command occurs directly in a theory. This is redundant. I now take this as a temporary solution until there is some better terminology for distinguishing kinds of interpretations, and I very much hope that we will not get into another debate about renaming 'interpretation' to 'global_interpretation' or similar after the 2016 release. I am personally very comfortable with the situation »as it is« by now and I am convinced there is now much time to breathe before we have to make any final decisions on that matter. Enjoy your time, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_23-Dec-2015
Just a casual user experience report. In the last days I brought some ancient patches from my queue into shape (definitely nothing for the next release) and this involved a lot of proof tuning (sometimes also termination issues) scattered over many theories in the distribution and the afp. I am working on not-so-up-to-date hardware. It was quite simple to carry that out – in the past there was always a risk that a couple of non-terminating proofs would (practically) block the ui. Now I had experienced this only once. Very convincing! Cheers, Florian Am 23.12.2015 um 22:55 schrieb Makarius: > Here is another Isabelle test snapshot: > http://www4.in.tum.de/~wenzelm/test/Isabelle_23-Dec-2015 > > It contains an updated version of Poly/ML as an approximation of version > 5.6 that David Matthews is preparing for the beginning of 2016. > > After the Christmas break, there will be further moves towards the > Isabelle2016 release. Hopefully, Oracle will manage to keep its own > schedule for the next Java 8 release on 19-Jan-2016: > https://www.java.com/en/download/faq/release_dates.xml > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
