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 |