| Tue, 03 Jul 2007 21:56:25 +0200 |
paulson |
to handle non-atomic assumptions
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 17:34:44 +0200 |
paulson |
Added flexflex_first_order and tidied first_order_resolution
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 19:22:01 +0200 |
haftmann |
eliminated Code_Generator.thy
|
file |
diff |
annotate
|
| Tue, 08 May 2007 17:40:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 18 Apr 2007 11:14:09 +0200 |
paulson |
Fixes for proof reconstruction, especially involving abstractions and definitions
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 13:58:47 +0200 |
paulson |
Zero variable indexes in clauses
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 11:12:39 +0200 |
paulson |
MESON tactical takes an additional argument: the clausification function.
|
file |
diff |
annotate
|
| Mon, 26 Mar 2007 12:46:27 +0200 |
paulson |
"generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 12:35:20 +0100 |
paulson |
The first-order test now tests for the obscure case of a polymorphic constant like 1 being
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:14 +0100 |
wenzelm |
Output.debug: non-strict;
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
file |
diff |
annotate
|
| Fri, 22 Dec 2006 21:00:42 +0100 |
paulson |
tidying the ATP communications
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:18:55 +0100 |
wenzelm |
LocalDefs.expand;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2006 12:23:39 +0100 |
paulson |
Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 19:25:41 +0100 |
wenzelm |
removed is_Trueprop (use can dest_Trueprop'' instead);
|
file |
diff |
annotate
|
| Thu, 26 Oct 2006 10:48:35 +0200 |
paulson |
Conversion to clause form now tolerates Boolean variables without looping.
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 11:17:29 +0200 |
paulson |
Improved tracing
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 11:03:33 +0200 |
paulson |
nclauses no longer requires its input to be in NNF
|
file |
diff |
annotate
|
| Wed, 18 Oct 2006 10:15:39 +0200 |
paulson |
More robust error handling in make_nnf and forward_res
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 10:49:36 +0200 |
haftmann |
abandoned findrep
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 17:29:42 +0200 |
paulson |
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:17:17 +0200 |
paulson |
Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
|
file |
diff |
annotate
|
| Fri, 25 Aug 2006 18:47:36 +0200 |
paulson |
better skolemization, using first-order resolution rather than hoping for the right result
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 18:40:20 +0200 |
paulson |
more explict variable names
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:40 +0200 |
wenzelm |
simplified Assumption/ProofContext.export;
|
file |
diff |
annotate
|
| Sun, 16 Jul 2006 14:26:22 +0200 |
paulson |
has_consts renamed to has_conn, now actually parses the first-order formula
|
file |
diff |
annotate
|