[isabelle-dev] NEWS

[Sascha Boehme]

The SMT solver Z3 has now by default a restricted set of directly  
supported features. For the full set of features (div/mod, nonlinear  
arithmetic, datatypes/records) with potential proof reconstruction  
failures, enable the configuration option "z3_with_extensions". Minor  
INCOMPATIBILITY.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev