src/HOL/Tools/SMT/smt_datatypes.ML
Mon, 15 Dec 2014 07:20:48 +0100 blanchet avoid generating selectors with function types -- this produce arity inconsistencies
Thu, 20 Nov 2014 17:29:18 +0100 blanchet work around bug in CVC4, with boolean arguments to (co)datatypes
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
Fri, 26 Sep 2014 14:41:54 +0200 desharna refactor fp_sugar move theorems
Wed, 24 Sep 2014 15:46:40 +0200 blanchet allow homogeneous nesting for SMT (co)datatypes
Wed, 24 Sep 2014 15:46:25 +0200 blanchet interleave (co)datatypes in the right order w.r.t. dependencies
Wed, 24 Sep 2014 15:46:24 +0200 blanchet rule out nested (co)recursion for SMT (co)datatypes
Wed, 24 Sep 2014 15:46:23 +0200 blanchet gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
Wed, 17 Sep 2014 23:45:57 +0200 blanchet tuning
Wed, 17 Sep 2014 21:35:58 +0200 blanchet register Isabelle selectors as SMT selectors when possible
Wed, 17 Sep 2014 17:32:27 +0200 blanchet added codatatype support for CVC4
Wed, 17 Sep 2014 16:53:39 +0200 blanchet added interface for CVC4 extensions
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Thu, 12 Jun 2014 01:00:49 +0200 blanchet use 'ctr_sugar' abstraction in SMT(2)
Wed, 11 Jun 2014 11:28:46 +0200 blanchet fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
Tue, 14 Jun 2011 13:50:54 +0200 boehmes slightly more general treatment of mutually recursive datatypes;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Mon, 03 Jan 2011 16:22:08 +0100 boehmes re-implemented support for datatypes (including records and typedefs);
less more (0) tip