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