| Mon, 07 Nov 2011 17:54:35 +0100 | boehmes | replace higher-order matching against schematic theorem with dedicated reconstruction method | file | diff | annotate |
| Tue, 25 Oct 2011 08:48:36 +0200 | boehmes | clarify types of terms: use proper set type | file | diff | annotate |
| Wed, 09 Mar 2011 21:40:38 +0100 | boehmes | finished and tested Z3 proof reconstruction for injective functions; | file | diff | annotate |
| Mon, 20 Dec 2010 22:02:57 +0100 | boehmes | avoid ML structure aliases (especially single-letter abbreviations) | file | diff | annotate |
| Wed, 01 Dec 2010 13:09:08 +0100 | wenzelm | just one Term.dest_funT; | file | diff | annotate |
| Mon, 22 Nov 2010 15:45:43 +0100 | boehmes | share and use more utility functions; | file | diff | annotate |
| Mon, 22 Nov 2010 15:45:42 +0100 | boehmes | added prove reconstruction for injective functions; | file | diff | annotate |