Something slightly related and not very important. In changeset
9ff441f295c2 of the Isabelle repo the congruence rule for the constant
"list_ex" is called list_any_cong. For consistency I suggest to rename
it to list_ex_cong.
cheers
chris
On 03/16/2012 06:47 PM, Christian Sternagel wrote:
Dear all,
in preparation for the next release I refactored one of our AFP entries
(Abstract-Rewriting). There was an underlying theory Util.thy (quite
big), which essentially turned out to be unused in the rest of the AFP
entry ;) (but we heavily rely on it in IsaFoR, which is not in the AFP).
While refactoring I saw that some lemmas from Util.thy have found their
way (either by moving or independently) into the main Isabelle
distribution (mostly List.thy) -- but without being removed from the AFP
entry.
Still there are many definitions and lemmas left that are not part of
the main distribution (some of which are ugly and ad hoc, but others
quite useful and maybe deserving to end up in the distribution or library).
After this rather long story ;) my actual question: Is there some way to
propose definitions/lemmas for the main distribution/library? If not,
maybe someone of the developers feels like reading through the attached
theory-file and picking out whatever he/she likes?
cheers
chris
On 02/28/2012 10:21 PM, Makarius wrote:
Dear all,
4 months after Isabelle2011-1 we are roughly in the middle between two
official releases. This is a good point to recollect things for the
coming release, better than a few weeks before actual rollout (which
will the time for testing the integrated system, not adding new
features).
After 3.4 weeks vacation in Marokko in Jan/Feb and 2 weeks working
through my mail folders like crazy, I still have issues in the pipeline
that need to be reanimated. I also need to figure out which essential
things of the Prover IDE can make it into the release ...
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
