isabelle: Changelog

wenzelm [Wed, 15 Jan 2014 19:02:58 +0100] rev 55013

merged

wenzelm [Wed, 15 Jan 2014 16:57:29 +0100] rev 55012

fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;

nipkow [Wed, 15 Jan 2014 16:59:24 +0100] rev 55011

tuned text

nipkow [Wed, 15 Jan 2014 08:01:36 +0100] rev 55010

tuned

blanchet [Tue, 14 Jan 2014 18:41:24 +0100] rev 55009

automatically solve proof obligations produced for code equations

blanchet [Tue, 14 Jan 2014 18:41:24 +0100] rev 55008

use 'disc_exhausts' property both from types on which 'case's take place and on return type

wenzelm [Mon, 13 Jan 2014 20:20:44 +0100] rev 55007

activation of Z3 via "z3_non_commercial" system option (without requiring restart);

wenzelm [Mon, 13 Jan 2014 18:47:48 +0100] rev 55006

tuned;

blanchet [Mon, 13 Jan 2014 14:11:02 +0100] rev 55005

use the right context in 'unfold_thms id_def'

blanchet [Mon, 13 Jan 2014 13:24:09 +0100] rev 55004

repaired 'ctr' tactic w.r.t. 'split'

isabelle