isabelle: File revisions

src/HOL/SMT_Examples/SMT_Examples.thy

Thu, 13 Mar 2014 14:55:38 +0100	blanchet	updated SMT example certificates	file \| diff \| annotate
Thu, 13 Mar 2014 13:18:13 +0100	blanchet	use 'smt2' in SMT examples as much as currently possible	file \| diff \| annotate
Fri, 14 Feb 2014 07:53:45 +0100	blanchet	merged 'List.map' and 'List.list.map'	file \| diff \| annotate
Wed, 02 Jan 2013 09:31:25 +0100	blanchet	actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled	file \| diff \| annotate
Mon, 04 Jun 2012 09:07:23 +0200	boehmes	restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"	file \| diff \| annotate
Tue, 27 Mar 2012 17:11:02 +0200	boehmes	dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct	file \| diff \| annotate
Tue, 27 Mar 2012 16:59:13 +0300	blanchet	renamed "smt_fixed" to "smt_read_only_certificates"	file \| diff \| annotate

isabelle