| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Wed, 13 Feb 2008 15:14:17 +0100 |
paulson |
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 18:39:00 +0100 |
paulson |
Skolemization now catches exception THM, which may be raised if unification fails.
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 18:14:00 +0200 |
paulson |
context-based treatment of generalization; also handling TFrees in axiom clauses
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 12:32:58 +0200 |
paulson |
combinator translation
|
file |
diff |
annotate
|
| Thu, 27 Sep 2007 17:55:28 +0200 |
paulson |
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 00:03:50 +0200 |
wenzelm |
proper signature for Meson;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:56 +0200 |
wenzelm |
proper simproc_setup for "neq", "let_simp";
|
file |
diff |
annotate
|
| Sat, 21 Jul 2007 23:25:00 +0200 |
wenzelm |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:26 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
file |
diff |
annotate
|
| 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
|
| Thu, 13 Jul 2006 12:31:00 +0200 |
paulson |
fix to refl_clause_aux: added occurs check
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:58 +0200 |
wenzelm |
removed obsolete mem_term;
|
file |
diff |
annotate
|
| Wed, 05 Jul 2006 16:24:28 +0200 |
paulson |
removed the "tagging" feature
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 17:50:47 +0200 |
paulson |
the "all_theorems" option and some fixes
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:37 +0200 |
wenzelm |
avoid unqualified exception names;
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:02 +0200 |
wenzelm |
freeze_spec: gensym;
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 16:45:04 +0100 |
paulson |
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
|
file |
diff |
annotate
|
| Tue, 28 Feb 2006 11:09:29 +0100 |
paulson |
fixed but in freeze_spec
|
file |
diff |
annotate
|
| Mon, 20 Feb 2006 16:22:52 +0100 |
paulson |
Fix variable-naming bug (?) by removing a needless recursive call
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:51 +0100 |
wenzelm |
LocalDefs.def_export;
|
file |
diff |
annotate
|
| Mon, 23 Jan 2006 11:38:43 +0100 |
paulson |
Clausification now handles some IFs in rewrite rules (if-split did not work)
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:13 +0100 |
wenzelm |
Output.debug;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:12:58 +0100 |
wenzelm |
ProofContext.def_export;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 17:34:46 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 16:14:26 +0100 |
paulson |
removal of some redundancies (e.g. one-point-rules) in clause production
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 15:27:43 +0100 |
paulson |
removal of functional reflexivity axioms
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:05:11 +0100 |
mengj |
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
|
file |
diff |
annotate
|