| Wed, 12 May 2010 23:53:59 +0200 | boehmes | split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols) | file | diff | annotate |
| Wed, 12 May 2010 23:53:48 +0200 | boehmes | moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction) | file | diff | annotate |
| Mon, 26 Apr 2010 11:34:19 +0200 | haftmann | dropped group_simps, ring_simps, field_eq_simps | file | diff | annotate |
| Wed, 11 Nov 2009 15:43:03 +0100 | boehmes | changed URL of SMT server, | file | diff | annotate |
| Tue, 20 Oct 2009 15:03:17 +0200 | boehmes | additional schematic rules for Z3's rewrite rule | file | diff | annotate |
| Tue, 20 Oct 2009 10:11:30 +0200 | boehmes | added proof reconstructon for Z3, | file | diff | annotate |