[isabelle-dev] NEWS

2012-06-04 Thread 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

Re: [isabelle-dev] NEWS

2012-06-04 Thread Lars Noschinski 

On 04.06.2012 09:28, Sascha Boehme wrote:

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.


What is the reasoning behind this change?

  -- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] JinjaThreads does not compile

2012-06-04 Thread Andreas Lochbihler 

Hi Stefan,


while doing a testall on the AFP, I noticed that JinjaThreads no longer
compiles. I get the error

*** exception Match raised (line 146)
***
*** At command ML (line 145 of 
/mnt/home/berghofe/isabelle/afp/thys/JinjaThreads/Examples/BufferExample.thy)

This should be now fixed in Isabelle 02d64fd40852.

I also removed the obsolete reference to FinFun in JinjaThreads/Basic
(AFP b060f6386ebc).

Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev