| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sat, 25 Apr 2015 09:48:06 +0200 |
blanchet |
made CVC4 support work also without unsat cores
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2015 23:23:31 +0100 |
boehmes |
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
|
file |
diff |
annotate
|
| Thu, 15 Jan 2015 21:44:51 +0100 |
boehmes |
more detailed runtime statistics for Z3 proof reconstruction
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 22:14:13 +0100 |
boehmes |
optionally display statistics for Z3 proof reconstruction
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 14:57:13 +0100 |
boehmes |
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 18:37:33 +0200 |
blanchet |
simplified and repaired veriT index handling code
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
| base
|