src/HOL/Tools/SMT/smt_datatypes.ML
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