src/HOL/Tools/SMT/smt_datatypes.ML
2014-12-15 blanchet 2014-12-15 correctly apply type substitution before checking for function types
2014-12-15 blanchet 2014-12-15 avoid generating selectors with function types -- this produce arity inconsistencies
2014-11-20 blanchet 2014-11-20 work around bug in CVC4, with boolean arguments to (co)datatypes
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-24 blanchet 2014-09-24 allow homogeneous nesting for SMT (co)datatypes
2014-09-24 blanchet 2014-09-24 interleave (co)datatypes in the right order w.r.t. dependencies
2014-09-24 blanchet 2014-09-24 rule out nested (co)recursion for SMT (co)datatypes
2014-09-24 blanchet 2014-09-24 gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
2014-09-17 blanchet 2014-09-17 tuning
2014-09-17 blanchet 2014-09-17 register Isabelle selectors as SMT selectors when possible
2014-09-17 blanchet 2014-09-17 added codatatype support for CVC4
2014-09-17 blanchet 2014-09-17 added interface for CVC4 extensions
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-06-12 blanchet 2014-06-12 use 'ctr_sugar' abstraction in SMT(2)
2014-06-11 blanchet 2014-06-11 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
2011-06-14 boehmes 2011-06-14 slightly more general treatment of mutually recursive datatypes; treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-03 boehmes 2011-01-03 re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs