| Mon, 04 Oct 2010 09:05:15 +0200 |
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
|
file | diff | annotate |
| Fri, 01 Oct 2010 16:58:56 +0200 |
tune bound names
|
file | diff | annotate |
| Fri, 01 Oct 2010 15:34:09 +0200 |
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
|
file | diff | annotate |
| Fri, 01 Oct 2010 14:01:29 +0200 |
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
|
file | diff | annotate |
| Thu, 30 Sep 2010 00:29:37 +0200 |
move functions closer to where they're used
|
file | diff | annotate |
| Wed, 29 Sep 2010 22:23:27 +0200 |
first step towards a new skolemizer that doesn't require "Eps"
|
file | diff | annotate |
| Sat, 11 Sep 2010 12:31:58 +0200 |
tuning
|
file | diff | annotate |
| Fri, 10 Sep 2010 15:17:44 +0200 |
merged
|
file | diff | annotate |
| Thu, 09 Sep 2010 18:04:35 +0200 |
Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;
|
file | diff | annotate |
| Thu, 09 Sep 2010 20:11:52 +0200 |
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
|
file | diff | annotate |
| Mon, 06 Sep 2010 19:13:10 +0200 |
more antiquotations;
|
file | diff | annotate |
| Thu, 02 Sep 2010 13:18:19 +0200 |
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
|
file | diff | annotate |
| Sat, 28 Aug 2010 16:14:32 +0200 |
formerly unnamed infix equality now named HOL.eq
|
file | diff | annotate |
| Fri, 27 Aug 2010 17:11:29 +0200 |
more appropriate name for configuration option "meson_max_clauses" (cf. output of 'pront_configs');
|
file | diff | annotate |
| Fri, 27 Aug 2010 16:29:12 +0200 |
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
|
file | diff | annotate |
| Fri, 27 Aug 2010 10:56:46 +0200 |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file | diff | annotate |
| Thu, 26 Aug 2010 20:51:17 +0200 |
formerly unnamed infix impliciation now named HOL.implies
|
file | diff | annotate |
| Wed, 25 Aug 2010 15:12:49 +0200 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| Fri, 20 Aug 2010 20:29:50 +0200 |
merged
|
file | diff | annotate |
| Fri, 20 Aug 2010 17:48:30 +0200 |
split and enriched theory SetsAndFunctions
|
file | diff | annotate |
| Fri, 20 Aug 2010 14:18:55 +0200 |
merged
|
file | diff | annotate |
| Fri, 20 Aug 2010 10:58:01 +0200 |
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
|
file | diff | annotate |
| Thu, 19 Aug 2010 18:16:47 +0200 |
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
|
file | diff | annotate |
| Thu, 19 Aug 2010 16:08:54 +0200 |
more antiquotations
|
file | diff | annotate |
| Thu, 19 Aug 2010 11:02:14 +0200 |
use antiquotations for remaining unqualified constants in HOL
|
file | diff | annotate |
| Thu, 29 Jul 2010 22:13:15 +0200 |
fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
|
file | diff | annotate |
| Thu, 29 Jul 2010 16:41:32 +0200 |
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
|
file | diff | annotate |
| Wed, 21 Jul 2010 21:15:07 +0200 |
renamings + only need second component of name pool to reconstruct proofs
|
file | diff | annotate |
| Mon, 12 Jul 2010 21:38:37 +0200 |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file | diff | annotate |
| Thu, 24 Jun 2010 17:25:47 +0200 |
cosmetics
|
file | diff | annotate |
| Mon, 14 Jun 2010 10:36:01 +0200 |
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 |
beta-eta-contract, to respect "first_order_match"'s specification;
|
file | diff | annotate |
| Tue, 08 Jun 2010 16:37:22 +0200 |
tuned quotes, antiquotations and whitespace
|
file | diff | annotate |
| Fri, 30 Apr 2010 23:53:37 +0200 |
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 |
static defaults for configuration options;
|
file | diff | annotate |
| Mon, 22 Mar 2010 10:25:44 +0100 |
merged
|
file | diff | annotate |
| Mon, 22 Mar 2010 10:25:07 +0100 |
start work on direct proof reconstruction for Sledgehammer
|
file | diff | annotate |
| Sat, 20 Mar 2010 17:33:11 +0100 |
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 |
modernized structure Object_Logic;
|
file | diff | annotate |
| Sun, 28 Feb 2010 23:51:31 +0100 |
more antiquotations;
|
file | diff | annotate |
| Thu, 28 Jan 2010 11:48:49 +0100 |
new theory Algebras.thy for generic algebraic structures
|
file | diff | annotate |
| Sat, 21 Nov 2009 15:49:29 +0100 |
explicitly mark some legacy freeze operations;
|
file | diff | annotate |
| Thu, 29 Oct 2009 23:56:33 +0100 |
eliminated some old folds;
|
file | diff | annotate |
| Thu, 29 Oct 2009 17:58:26 +0100 |
standardized filter/filter_out;
|
file | diff | annotate |
| Tue, 27 Oct 2009 22:56:14 +0100 |
eliminated some old folds;
|
file | diff | annotate |
| Tue, 27 Oct 2009 13:15:20 +0100 |
critical comments;
|
file | diff | annotate |
| Sat, 17 Oct 2009 14:43:18 +0200 |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file | diff | annotate |
| Fri, 16 Oct 2009 10:45:10 +0200 |
local channels for tracing/debugging;
|
file | diff | annotate |
| Tue, 29 Sep 2009 16:24:36 +0200 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| Thu, 30 Jul 2009 12:20:43 +0200 |
qualified Subgoal.FOCUS;
|
file | diff | annotate |
| Wed, 29 Jul 2009 19:35:10 +0200 |
Meson.first_order_resolve: avoid handle _;
|
file | diff | annotate |
| Mon, 27 Jul 2009 20:45:40 +0200 |
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 |
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 |
tuned/modernized Envir operations;
|
file | diff | annotate |
| Mon, 06 Jul 2009 21:24:30 +0200 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| Thu, 04 Jun 2009 15:28:58 +0200 |
dropped legacy ML bindings; tuned
|
file | diff | annotate |
| Fri, 20 Mar 2009 15:24:18 +0100 |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file | diff | annotate |
| Sun, 01 Mar 2009 23:36:12 +0100 |
use long names for old-style fold combinators;
|
file | diff | annotate |
| Thu, 29 Jan 2009 12:05:19 +0000 |
Minor reorganisation of the Skolemization code
|
file | diff | annotate |
| Wed, 31 Dec 2008 00:08:13 +0100 |
use exists_subterm directly;
|
file | diff | annotate |