| Mon, 14 Jun 2010 10:36:01 +0200 |
blanchet |
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:07:27 +0200 |
blanchet |
beta-eta-contract, to respect "first_order_match"'s specification;
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:22 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 23:53:37 +0200 |
wenzelm |
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 10:25:44 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 10:25:07 +0100 |
blanchet |
start work on direct proof reconstruction for Sledgehammer
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 15:49:29 +0100 |
wenzelm |
explicitly mark some legacy freeze operations;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:56:33 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 22:56:14 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 13:15:20 +0100 |
wenzelm |
critical comments;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 10:45:10 +0200 |
wenzelm |
local channels for tracing/debugging;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 19:35:10 +0200 |
wenzelm |
Meson.first_order_resolve: avoid handle _;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 20:45:40 +0200 |
wenzelm |
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:28:58 +0200 |
haftmann |
dropped legacy ML bindings; tuned
|
file |
diff |
annotate
|
| 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
|
| 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
|