[isabelle-dev] Isabelle services not available this weekend (2015-07-03 to 2015-07-06)
Hi everyone, due to maintenance of the power grid at TU Munich, a number of Isabelle related services will not be available this weekend (starting Friday, July 3th, 9:00 CEST to Monday, July 6th, somewhere in the afternoon CEST), in particular - the isabelle-dev mailing list, - the development repositories, - and the Munich mirror of the website[1]. The isabelle-users mailing list is hosted in Cambridge and thus not affected. -- Lars [1] The mirrors at Cambridge and Sydney are not affected: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html http://mirror.cse.unsw.edu.au/pub/isabelle/index.html ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: cases from goals
On Fri, 26 Jun 2015, Larry Paulson wrote: Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a while. AFP probably has a few thousand. I did not even check before sorting out this old problem from more than 10 years ago. It could have been addressed earlier, then there would have been less work to eliminate it now. Generally, there are more things that can be improved on Isar proofs, using the new facilities like 'consider' and 'have' / 'show' with eigen-context. Quite often, the elimination of awkward goal42(17) proofs actually uses that instead of falling back on the new goals method. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Deprecating legacy ASCII symbols?
Dear list, the following mail may contain a stupid idea. In HOL.thy, the conjunction (conj) is first introduced with the symbol. Later, the notation ∧ is introduced. In order to clean up this difficult-to-understand theory, would it be possible to directly introduce conjunction with the ∧ symbol? I see three advantages: 1) It simplifies the axiomatizations (a very critical part). 2) It may help in getting started with Isabelle since no confusing symbol would appear anywhere. Currently, if a ctrl-click on a lemma sends me to HOL.thy, things look pretty scary. 3) It would free up the symbol for custom theories. This could also be done for %, --, ==, ~, and many more. I guess this would break a lot, that's why I'm posting on dev. Best, Cornelius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
