| Fri, 06 Mar 2015 23:44:57 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sun, 21 Dec 2014 15:03:45 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
use context instead of theory
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
removed final periods in messages for proof methods
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 21:09:53 +0100 |
wenzelm |
more standard file/module names;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 18:42:46 +0100 |
wenzelm |
proper context for printing;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
make higher-order goals more first-order via extensionality
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
added "ext_cong_neq" lemma (not used yet); tuning
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:40:06 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
added unfold set constant functionality to Meson/Metis -- disabled by default for now
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
remove needless export
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
improve definitional CNF on goal by moving "not" past the quantifiers
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
experiment with definitional CNF
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
try to repair out-of-sync situations in Metis
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 12:16:25 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Sat, 26 Mar 2011 15:55:22 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
avoid evil "export_without_context", which breaks if there are local "fixes"
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more robust handling of variables in new Skolemizer
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 10:18:42 +0100 |
blanchet |
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 13:45:43 +0100 |
wenzelm |
refer to regular structure Simplifier;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
restructure Skolemization code slightly
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
more work on new Skolemizer without Hilbert_Choice
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:44:07 +0200 |
blanchet |
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:59:12 +0200 |
blanchet |
got rid of overkill "meson_choice" attribute;
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:30:50 +0200 |
blanchet |
more explicit name
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:28:11 +0200 |
blanchet |
factor out "Meson_Tactic" from "Meson_Clausify"
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:49:07 +0200 |
blanchet |
move Meson to Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:37:42 +0200 |
blanchet |
move MESON files together
|
file |
diff |
annotate
| base
|