| Wed, 06 Dec 2006 17:08:19 +0100 |
paulson |
Improved tracing
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:17:38 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 17:32:03 +0200 |
paulson |
Changing the default for theory_const
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 16:00:19 +0200 |
paulson |
Added the max_new parameter, which is a cap on how many clauses may be admitted per round.
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:21:35 +0200 |
paulson |
Added the "theory_const" option. Only it is OFF because it's often harmful!
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:51:53 +0200 |
paulson |
refinements to conversion into clause form, esp for the HO case
|
file |
diff |
annotate
|
| Mon, 28 Aug 2006 18:18:31 +0200 |
paulson |
minor bug fixes
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:04 +0200 |
wenzelm |
use Term.add_vars instead of obsolete term_varnames;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 11:55:26 +0200 |
paulson |
Fixed the bugs introduced by the last commit! Output is now *identical* to that
|
file |
diff |
annotate
|
| Sat, 15 Jul 2006 15:26:50 +0200 |
paulson |
Replaced a-lists by tables to improve efficiency
|
file |
diff |
annotate
|
| Wed, 19 Apr 2006 10:43:09 +0200 |
paulson |
definition expansion checks for excess variables
|
file |
diff |
annotate
|
| Fri, 07 Apr 2006 05:14:06 +0200 |
mengj |
filter now accepts axioms as thm, instead of term.
|
file |
diff |
annotate
|
| Wed, 05 Apr 2006 12:47:38 +0200 |
paulson |
pool of constants; definition expansion; current best settings
|
file |
diff |
annotate
|
| Fri, 31 Mar 2006 10:52:20 +0200 |
paulson |
Removal of unused code
|
file |
diff |
annotate
|
| Tue, 28 Mar 2006 16:48:18 +0200 |
paulson |
Simplified version of Jia's filter. Now all constants are pooled, rather than
|
file |
diff |
annotate
|
| Thu, 23 Mar 2006 10:05:03 +0100 |
paulson |
detection of definitions of relevant constants
|
file |
diff |
annotate
|
| Wed, 22 Mar 2006 12:30:29 +0100 |
paulson |
Removal of obsolete strategies. Initial support for locales: Frees and Consts
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 12:27:36 +0100 |
paulson |
Frequency analysis of constants (with types).
|
file |
diff |
annotate
|
| Wed, 08 Mar 2006 10:19:57 +0100 |
paulson |
Frequency strategy. Revised indentation, etc.
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 16:49:48 +0100 |
paulson |
Tidying and restructuring.
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 04:04:21 +0100 |
mengj |
relevance_filter takes input axioms as Term.term.
|
file |
diff |
annotate
|
| Mon, 13 Feb 2006 14:05:43 +0100 |
mengj |
Fixed a bug of type unification.
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 14:23:35 +0100 |
mengj |
Added another filter strategy.
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 05:34:20 +0100 |
mengj |
Relevance filtering. Has replaced the previous version.
|
file |
diff |
annotate
|