src/HOL/Tools/meson.ML
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;
Mon, 29 Sep 2008 11:46:47 +0200 wenzelm handle _ should be avoided (spurious Interrupt will spoil the game);
Tue, 09 Sep 2008 16:16:20 +0200 paulson more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Mon, 16 Jun 2008 17:54:43 +0200 wenzelm RuleInsts.read_instantiate;
Wed, 11 Jun 2008 18:02:00 +0200 wenzelm Drule.read_instantiate;
Sat, 17 May 2008 15:31:42 +0200 wenzelm cat_lines;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
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.
Thu, 27 Mar 2008 14:41:09 +0100 wenzelm eliminated theory ProtoPure;
Wed, 13 Feb 2008 15:14:17 +0100 paulson make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
Wed, 19 Dec 2007 17:40:48 +0100 paulson Replaced refs by config params; finer critical section in mets method
Tue, 18 Dec 2007 18:39:00 +0100 paulson Skolemization now catches exception THM, which may be raised if unification fails.
Tue, 09 Oct 2007 18:14:00 +0200 paulson context-based treatment of generalization; also handling TFrees in axiom clauses
Thu, 04 Oct 2007 12:32:58 +0200 paulson combinator translation
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
Fri, 17 Aug 2007 00:03:50 +0200 wenzelm proper signature for Meson;
Sun, 29 Jul 2007 14:29:56 +0200 wenzelm proper simproc_setup for "neq", "let_simp";
Sat, 21 Jul 2007 23:25:00 +0200 wenzelm tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
Thu, 05 Jul 2007 20:01:26 +0200 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
Tue, 03 Jul 2007 21:56:25 +0200 paulson to handle non-atomic assumptions
Wed, 20 Jun 2007 17:34:44 +0200 paulson Added flexflex_first_order and tidied first_order_resolution
Tue, 05 Jun 2007 19:22:01 +0200 haftmann eliminated Code_Generator.thy
Tue, 08 May 2007 17:40:18 +0200 wenzelm tuned;
Wed, 18 Apr 2007 11:14:09 +0200 paulson Fixes for proof reconstruction, especially involving abstractions and definitions
Thu, 12 Apr 2007 13:58:47 +0200 paulson Zero variable indexes in clauses
Thu, 29 Mar 2007 11:12:39 +0200 paulson MESON tactical takes an additional argument: the clausification function.
Mon, 26 Mar 2007 12:46:27 +0200 paulson "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
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
less more (0) -100 -60 tip