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 |