- Z3 is now always enabled by default, now that it is fully open
source. The "z3_non_commercial" option is discontinued.
In addition, Z3 should now (again) be invoked by default by Sledgehammer. Let
me know if you see anything odd, e.g. odd problems with binaries on Linux or
Windows.
Jasm
> The singleton constructor
> would be retained as an abbreviation for "insert_mset _ {#}"
Maybe even that won't be necessary since there is also explicit
enumeration syntax for multisets, AFAIR.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftm
On 02.04.2015 00:31, Makarius wrote:
> On http://isabelle.in.tum.de/reports/Isabelle there is very little to
> see. This is occasionally important to investigate timing problems, or
> to see how Isabelle vs. AFP works out.
The testbench suites were running, but none of the other tests. One
instan
Sounds logical to me.
Larry
> On 8 Apr 2015, at 08:13, Tobias Nipkow wrote:
>
> Currently the setup in Multiset is geared towards having the 3 basic
> (non-free) constructors: empty, singleton and union. Although induction
> already has only two cases (empty and union with singleton), it would
Currently the setup in Multiset is geared towards having the 3 basic (non-free)
constructors: empty, singleton and union. Although induction already has only
two cases (empty and union with singleton), it would be nicer to have only two
constructors, like for finite sets: empty and insert. In pa
