isabelle: File revisions

src/HOL/Tools/SMT/smt_datatypes.ML

Wed, 17 Sep 2014 21:35:58 +0200	blanchet	register Isabelle selectors as SMT selectors when possible	file \| diff \| annotate
Wed, 17 Sep 2014 17:32:27 +0200	blanchet	added codatatype support for CVC4	file \| diff \| annotate
Wed, 17 Sep 2014 16:53:39 +0200	blanchet	added interface for CVC4 extensions	file \| diff \| annotate
Thu, 28 Aug 2014 00:40:38 +0200	blanchet	renamed new SMT module from 'SMT2' to 'SMT'	file \| diff \| annotate \| base
Thu, 12 Jun 2014 01:00:49 +0200	blanchet	use 'ctr_sugar' abstraction in SMT(2)	file \| diff \| annotate
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	file \| diff \| annotate
Tue, 14 Jun 2011 13:50:54 +0200	boehmes	slightly more general treatment of mutually recursive datatypes;	file \| diff \| annotate
Sat, 16 Apr 2011 16:15:37 +0200	wenzelm	modernized structure Proof_Context;	file \| diff \| annotate
Mon, 03 Jan 2011 16:22:08 +0100	boehmes	re-implemented support for datatypes (including records and typedefs);	file \| diff \| annotate

isabelle