| Mon, 15 Dec 2014 07:20:49 +0100 |
blanchet |
correctly apply type substitution before checking for function types
|
file |
diff |
annotate
|
| Mon, 15 Dec 2014 07:20:48 +0100 |
blanchet |
avoid generating selectors with function types -- this produce arity inconsistencies
|
file |
diff |
annotate
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
work around bug in CVC4, with boolean arguments to (co)datatypes
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 15:46:40 +0200 |
blanchet |
allow homogeneous nesting for SMT (co)datatypes
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 15:46:25 +0200 |
blanchet |
interleave (co)datatypes in the right order w.r.t. dependencies
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 15:46:24 +0200 |
blanchet |
rule out nested (co)recursion for SMT (co)datatypes
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 15:46:23 +0200 |
blanchet |
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 23:45:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| 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
|