On Wed, 18 Apr 2012, Johannes Hölzl wrote:
When the testboard gives me green light I will tomorrow also push a
reworked Probability theory which only takes 2 min to build instead of 5
min as before. I also want to push a new version of the Floats which
uses the new lifting infrastructure.
Both changes do not change any ML files, and there are only smaller
changes to the HOL image, so I hope it is still okay to push this.
You still have this convergence interval of 2 weeks. I recommend to push
within 1 week, though, since there are usually fine points to be settled
afterwards.
Concerning the "new lifting infrastructure": I've seen many things
floating in the past few weeks, but it was never mentioned before, and is
not covered in NEWS. So my impression was it is not "user-relevant" for
this release, as the NEWS title calls it.
Also, there seem to be certain ongoing things with quotients that are
nowhere covered. The time to do so is now. Anything not wrapped for this
release, is for the one after it.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
