[isabelle-dev] NEWS

Sascha Boehme boehmes at in.tum.de
Mon Jun 4 09:28:11 CEST 2012

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  

More information about the isabelle-dev mailing list