| Mon, 31 Aug 2020 22:05:05 +0200 |
wenzelm |
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 09:16:19 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:56:43 +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
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:55:29 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 21:11:03 +0200 |
blanchet |
fixed some spelling mistakes
|
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
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 17:26:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 16:53:32 +0200 |
wenzelm |
more standard fold/fold_rev;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 16:31:53 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 16:11:14 +0200 |
wenzelm |
prefer existing beta_eta_conversion;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 15:51:55 +0200 |
wenzelm |
more standard names;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 15:02:33 +0200 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 14:37:06 +0200 |
wenzelm |
tuned -- prefer terminology of tactic / goal state;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 14:17:56 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 13:59:38 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
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
|
| Wed, 12 Sep 2012 23:18:26 +0200 |
wenzelm |
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 22:00:29 +0200 |
wenzelm |
eliminated some old material that is unused in the visible universe;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 15:50:13 +0200 |
wenzelm |
misc tuning and simplification;
|
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
|
| Wed, 15 Dec 2010 15:11:56 +0100 |
wenzelm |
avoid ML structure aliases (especially single-letter abbreviations);
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:29:41 +0100 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| Sat, 30 May 2009 13:12:15 +0200 |
wenzelm |
minimal signature cleanup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:32:27 +0100 |
wenzelm |
replaced archaic use of rep_ss by Simplifier.mksimps;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:02:12 +0100 |
wenzelm |
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
|
file |
diff |
annotate
| base
|