Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT_Examples/SMT_Examples.thy
Sun, 01 Oct 2017 15:17:43 +0200 blanchet updated SMT certificates and added one test file | diff | annotate
Fri, 28 Jul 2017 15:36:32 +0100 blanchet introduced option for nat-as-int in SMT file | diff | annotate
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t; file | diff | annotate
Mon, 28 Dec 2015 01:28:28 +0100 wenzelm more symbols; file | diff | annotate
Wed, 08 Apr 2015 19:05:57 +0200 blanchet updated certificates to latest Z3 (and took out one problem that no longer works) file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet updated SMT certificates file | diff | annotate
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section; file | diff | annotate
Thu, 18 Sep 2014 00:03:46 +0200 blanchet renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate
Tue, 19 Aug 2014 09:36:37 +0200 blanchet avoid old 'smt' method in examples file | diff | annotate
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 file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet adapted examples to changes in SMT triggers file | diff | annotate
Fri, 25 Apr 2014 22:13:17 +0200 blanchet use Z3 4.3.2 to fix most FIXMEs file | diff | annotate
Thu, 13 Mar 2014 16:17:14 +0100 blanchet updated SMT2 certificates file | diff | annotate
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
Mon, 26 Mar 2012 11:01:04 +0200 blanchet reintroduced broken proofs and regenerated certificates file | diff | annotate
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS) file | diff | annotate
Tue, 03 Jan 2012 18:33:17 +0100 blanchet regenerate SMT example certificates, to reflect "set" type constructor file | diff | annotate
Sat, 24 Dec 2011 15:53:11 +0100 haftmann commented out examples which choke on strict set/pred distinction file | diff | annotate
Mon, 07 Nov 2011 17:54:38 +0100 boehmes try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways file | diff | annotate
Mon, 18 Jul 2011 18:52:52 +0200 boehmes allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction) file | diff | annotate
Fri, 08 Apr 2011 19:04:08 +0200 boehmes fixed eta-expansion: use correct order to apply new bound variables file | diff | annotate
Fri, 08 Apr 2011 19:04:08 +0200 boehmes unfold and eta-contract let expressions before lambda-lifting to avoid bad terms file | diff | annotate
Fri, 08 Apr 2011 19:04:08 +0200 boehmes corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables file | diff | annotate
Mon, 21 Feb 2011 09:19:44 +0100 boehmes added test cases with quantifier occurring in first-order term positions file | diff | annotate
Mon, 17 Jan 2011 17:45:52 +0100 boehmes made Z3 the default SMT solver again file | diff | annotate
Mon, 20 Dec 2010 09:31:47 +0100 boehmes updated SMT certificates file | diff | annotate
Sun, 19 Dec 2010 18:55:21 +0100 boehmes updated SMT certificates file | diff | annotate
Wed, 15 Dec 2010 10:52:43 +0100 boehmes updated SMT certificates file | diff | annotate
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in file | diff | annotate
Fri, 12 Nov 2010 15:56:07 +0100 boehmes look for certificates relative to the theory file | diff | annotate
Fri, 29 Oct 2010 18:17:04 +0200 boehmes introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list file | diff | annotate
Tue, 26 Oct 2010 11:46:19 +0200 boehmes changed SMT configuration options; updated SMT certificates file | diff | annotate
Thu, 27 May 2010 14:55:53 +0200 boehmes use Z3's builtin support for div and mod file | diff | annotate
Wed, 26 May 2010 15:34:47 +0200 boehmes hide constants and types introduced by SMT, file | diff | annotate
Wed, 12 May 2010 23:54:06 +0200 boehmes updated SMT certificates file | diff | annotate
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable file | diff | annotate
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image file | diff | annotate
less more (0) tip
isabelle