src/HOL/Tools/Meson/meson_clausify.ML
Mon, 12 Aug 2019 11:16:10 +0200 wenzelm do not open ML structures;
Fri, 09 Aug 2019 17:14:49 +0200 wenzelm formal position for PThm nodes;
Tue, 04 Jun 2019 20:49:33 +0200 wenzelm tuned;
Tue, 04 Jun 2019 15:14:56 +0200 wenzelm misc tuning and clarification, notably wrt. flow of context;
Sat, 13 Apr 2019 22:06:40 +0200 wenzelm tuned signature;
Sat, 13 Apr 2019 21:43:41 +0200 wenzelm meson: more cterm operations;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Sat, 25 Jul 2015 23:41:53 +0200 wenzelm updated to infer_instantiate;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Mon, 01 Jun 2015 13:35:16 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 23:44:57 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sun, 21 Dec 2014 15:03:45 +0100 wenzelm proper context;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Tue, 01 Jul 2014 16:47:10 +0200 blanchet use context instead of theory
Thu, 01 May 2014 09:30:35 +0200 haftmann optional case enforcement
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sun, 16 Feb 2014 21:33:28 +0100 blanchet removed final periods in messages for proof methods
Sat, 01 Feb 2014 21:09:53 +0100 wenzelm more standard file/module names;
Sat, 01 Feb 2014 18:42:46 +0100 wenzelm proper context for printing;
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Thu, 03 Jan 2013 17:28:55 +0100 blanchet use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
Tue, 22 May 2012 16:59:27 +0200 blanchet make higher-order goals more first-order via extensionality
Tue, 22 May 2012 16:59:27 +0200 blanchet added "ext_cong_neq" lemma (not used yet); tuning
Tue, 13 Mar 2012 16:40:06 +0100 wenzelm prefer abs_def over def_raw;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Mon, 02 Jan 2012 14:12:20 +0100 blanchet killed unfold_set_const option that makes no sense now that set is a type constructor again
Fri, 02 Dec 2011 14:54:25 +0100 wenzelm more antiquotations;
Tue, 15 Nov 2011 22:13:39 +0100 blanchet continued implementation of lambda-lifting in Metis
Tue, 15 Nov 2011 22:13:39 +0100 blanchet started implementing lambda-lifting in Metis
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Mon, 25 Jul 2011 14:10:12 +0200 blanchet thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals
Thu, 12 May 2011 15:29:19 +0200 blanchet use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
Thu, 12 May 2011 15:29:19 +0200 blanchet added unfold set constant functionality to Meson/Metis -- disabled by default for now
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 14 Apr 2011 11:24:05 +0200 blanchet remove needless export
Thu, 14 Apr 2011 11:24:05 +0200 blanchet properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
Thu, 14 Apr 2011 11:24:04 +0200 blanchet improve definitional CNF on goal by moving "not" past the quantifiers
Thu, 14 Apr 2011 11:24:04 +0200 blanchet experiment with definitional CNF
Thu, 14 Apr 2011 11:24:04 +0200 blanchet try to repair out-of-sync situations in Metis
Thu, 07 Apr 2011 12:16:25 +0200 blanchet tuned comment
Sat, 26 Mar 2011 15:55:22 +0100 wenzelm merged
Thu, 24 Mar 2011 17:49:27 +0100 blanchet avoid evil "export_without_context", which breaks if there are local "fixes"
Thu, 24 Mar 2011 17:49:27 +0100 blanchet more robust handling of variables in new Skolemizer
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Wed, 23 Mar 2011 10:18:42 +0100 blanchet avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
less more (0) -60 tip