isabelle: Changelog

blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56083

have Sledgehammer generate Isar proofs from Z3 proofs

blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56082

tuned ML interface

blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56081

integrate SMT2 with Sledgehammer

blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56080

removed tracing output

blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56079

use 'smt2' in SMT examples as much as currently possible

blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56078

moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle

haftmann [Thu, 13 Mar 2014 08:56:08 +0100] rev 56077

tuned proofs

haftmann [Thu, 13 Mar 2014 08:56:08 +0100] rev 56076

dropped redundant theorems

haftmann [Thu, 13 Mar 2014 08:56:08 +0100] rev 56075

tuned

haftmann [Thu, 13 Mar 2014 08:56:07 +0100] rev 56074

monotonicity in complete lattices

isabelle