| Tue, 12 May 2015 08:48:11 +0200 |
nipkow |
this warning is hardly useful but produces noisy markers in the jedit interface
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 16:09:55 +0100 |
nipkow |
rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
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
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
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
|
| Sat, 01 Nov 2014 11:40:55 +0100 |
wenzelm |
eliminated former Proof General preferences;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:17:56 +0100 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 12:01:32 +0200 |
wenzelm |
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 21:27:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 13:04:08 +0100 |
wenzelm |
more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example:
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 09:04:59 +0000 |
Lars Hupel |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
|
file |
diff |
annotate
|
| Fri, 17 Jan 2014 20:51:36 +0100 |
wenzelm |
back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2014 20:36:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2014 18:12:35 +0100 |
wenzelm |
clarified Simplifier diagnostics -- simplified ML;
|
file |
diff |
annotate
|
| Wed, 15 Jan 2014 22:24:57 +0100 |
wenzelm |
general notion of auxiliary bounds within context;
|
file |
diff |
annotate
|
| Sun, 12 Jan 2014 18:34:00 +0100 |
wenzelm |
proper context for clear_simpset: preserve dounds, depth;
|
file |
diff |
annotate
|
| Sun, 12 Jan 2014 13:16:00 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 21:37:28 +0100 |
wenzelm |
more elementary management of declared hyps, below structure Assumption;
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 16:55:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 14:29:22 +0100 |
wenzelm |
clarified simplifier context;
|
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, 12 Dec 2013 22:38:25 +0100 |
wenzelm |
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 21:14:33 +0100 |
wenzelm |
generic trace operations for main steps of Simplifier;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 17:34:50 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 16:56:53 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 16:17:35 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 14:35:31 +0100 |
wenzelm |
removed dead code -- ctxt is never visible (see also 658fcba35ed7);
|
file |
diff |
annotate
|
| Thu, 30 May 2013 13:07:23 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 20:49:10 +0200 |
wenzelm |
more rigorous check of simplifier context;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 14:04:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 17:39:38 +0200 |
wenzelm |
tuned signature -- depend on context by default;
|
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, 04 Apr 2013 10:30:28 +0200 |
nipkow |
removed unnerving (esp in jedit) and pointless warning
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 17:27:21 +0100 |
wenzelm |
amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 17:13:21 +0100 |
wenzelm |
more formal cong_name;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sat, 31 Mar 2012 19:26:23 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 15:42:07 +0100 |
wenzelm |
eliminated odd comment from distant past;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 19:29:54 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 17:51:29 +0100 |
wenzelm |
eliminated unused rewrite_goal_rule;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 17:26:35 +0100 |
wenzelm |
eliminated obsolete aliases;
|
file |
diff |
annotate
|
| Wed, 11 Jan 2012 16:25:34 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 23:07:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2011 12:03:51 +0100 |
wenzelm |
eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 13:07:47 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|