| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2009 12:05:19 +0000 |
paulson |
Minor reorganisation of the Skolemization code
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use exists_subterm directly;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 11:46:47 +0200 |
wenzelm |
handle _ should be avoided (spurious Interrupt will spoil the game);
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 16:16:20 +0200 |
paulson |
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:39 +0200 |
wenzelm |
pervasive RuleInsts;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:43 +0200 |
wenzelm |
RuleInsts.read_instantiate;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:02:00 +0200 |
wenzelm |
Drule.read_instantiate;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 15:31:42 +0200 |
wenzelm |
cat_lines;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2008 15:37:27 +0200 |
paulson |
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
|
file |
diff |
annotate
|
| 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
|