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