On Thu, 3 Jan 2013, Jasmin Blanchette wrote:
Hence, Sascha and I will look at the issue, and at any Z3 4.x-specific
issues, after the release.
On the other hand, he has a change to the monomorphizer in the pipeline
since October and might be able to introduce some enhancements in the
coming days (to make it more complete -- i.e. generate monomorphic
instances that previously were strangely forgotten). We'll proceed by
steps there, first upgrading the "smt" method, then Sledgehammer. The
change should be fairly straightforward; should there be any issues, we
can postpone it to after the release.
OK, just keep me informed once you know if it will be before or after the
release.
I hope to make a initial "test" snapshot within 1-2 days/weeks, and start
the actual "RC" phase before the end of January. The latter means the
usual fork to a restricted isabelle-release repository with public testing
and only important fixes accepted.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
