src/HOL/SMT_Examples/SMT_Examples.thy
Wed, 08 Apr 2015 19:05:57 +0200 blanchet updated certificates to latest Z3 (and took out one problem that no longer works)
Mon, 24 Nov 2014 12:35:13 +0100 blanchet updated SMT certificates
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 18 Sep 2014 00:03:46 +0200 blanchet renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Tue, 19 Aug 2014 09:36:37 +0200 blanchet avoid old 'smt' method in examples
Sun, 27 Jul 2014 21:11:35 +0200 blanchet do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
Thu, 12 Jun 2014 01:00:49 +0200 blanchet adapted examples to changes in SMT triggers
Fri, 25 Apr 2014 22:13:17 +0200 blanchet use Z3 4.3.2 to fix most FIXMEs
Thu, 13 Mar 2014 16:17:14 +0100 blanchet updated SMT2 certificates
Thu, 13 Mar 2014 14:55:38 +0100 blanchet updated SMT example certificates
Thu, 13 Mar 2014 13:18:13 +0100 blanchet use 'smt2' in SMT examples as much as currently possible
Fri, 14 Feb 2014 07:53:45 +0100 blanchet merged 'List.map' and 'List.list.map'
Wed, 02 Jan 2013 09:31:25 +0100 blanchet actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
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"
less more (0) -15 tip