#
2d8a20d9 |
|
22-Jan-2020 |
haftmann <none@none> |
tuned
|
#
ae353c5d |
|
19-Dec-2019 |
wenzelm <none@none> |
proper proof body context for Simplifier plugins (solvers, loopers, ...) -- avoid crash due to Subgoal.FOCUS (before e58bc223f46c);
|
#
1414eda3 |
|
04-Dec-2019 |
haftmann <none@none> |
proper table data structure --HG-- extra : rebase_source : 74bb8ec99405ac13dce51747a70bb95859ed216c
|
#
450e4fbf |
|
05-Dec-2019 |
haftmann <none@none> |
more direct accessors for simpset
|
#
bc634f57 |
|
04-Dec-2019 |
haftmann <none@none> |
regular merge with no historization, in accordance with regular update --HG-- extra : rebase_source : 6ff04e75725b6899116318ba26adcfc3f80da070
|
#
577c0313 |
|
28-Nov-2019 |
wenzelm <none@none> |
more structural integrity;
|
#
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
45adb6d5 |
|
14-Aug-2019 |
wenzelm <none@none> |
treat simproc results as atomic -- more compact proof terms;
|
#
cd87aa9a |
|
06-Aug-2019 |
wenzelm <none@none> |
more robust and convenient treatment of implicit context;
|
#
0e5c06bc |
|
03-Jan-2019 |
wenzelm <none@none> |
clarified signature: more types;
|
#
2b6e4b97 |
|
08-Oct-2018 |
Lars Hupel <lars.hupel@mytum.de> |
Jenkins: run ocaml_setup --HG-- extra : amend_source : 5f7c19b527752c7b3910480f59c0ef874d912dea
|
#
409b56ed |
|
07-Jun-2018 |
nipkow <none@none> |
comments
|
#
2b1ecb7f |
|
06-Jun-2018 |
nipkow <none@none> |
reorient -> split; documented split
|
#
b402d35b |
|
26-Apr-2018 |
nipkow <none@none> |
new simp modifier: reorient
|
#
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap; tuned comments;
|
#
ba9cb2ae |
|
18-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
9dda44c3 |
|
01-Feb-2018 |
wenzelm <none@none> |
clarified signature: prefer proper order operation;
|
#
85fed98b |
|
29-Oct-2017 |
nipkow <none@none> |
reduced simp_depth_limit
|
#
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
#
9619db56 |
|
02-Jun-2016 |
wenzelm <none@none> |
avoid warnings on duplicate rules in the given list;
|
#
81b459a5 |
|
08-Apr-2016 |
wenzelm <none@none> |
eliminated unused simproc identifier;
|
#
d70d74b6 |
|
05-Apr-2016 |
wenzelm <none@none> |
clarified modules -- simplified bootstrap;
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
e2360983 |
|
02-Sep-2015 |
wenzelm <none@none> |
eliminated pointless cterms;
|
#
56675b9c |
|
02-Sep-2015 |
wenzelm <none@none> |
trim context for persistent storage;
|
#
fa148bfd |
|
02-Sep-2015 |
wenzelm <none@none> |
more thorough transfer;
|
#
f2fe59c2 |
|
31-Aug-2015 |
wenzelm <none@none> |
routine check of theory context;
|
#
a86b3912 |
|
30-Aug-2015 |
wenzelm <none@none> |
trim context for persistent storage;
|
#
4125d2fe |
|
28-Jul-2015 |
wenzelm <none@none> |
more explicit context;
|
#
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
#
8f453cab |
|
01-Jun-2015 |
wenzelm <none@none> |
tuned;
|
#
0d557c40 |
|
12-May-2015 |
nipkow <none@none> |
this warning is hardly useful but produces noisy markers in the jedit interface
|
#
faf525fb |
|
13-Mar-2015 |
nipkow <none@none> |
rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
|
#
c97e9ad6 |
|
07-Mar-2015 |
wenzelm <none@none> |
clarified Drule.gen_all: observe context more carefully;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
16b4f761 |
|
08-Nov-2014 |
wenzelm <none@none> |
optional proof context for unify operations, for the sake of proper local options;
|
#
fcc41d2e |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated former Proof General preferences;
|
#
677c12ca |
|
30-Oct-2014 |
wenzelm <none@none> |
tuned spelling;
|
#
27c03196 |
|
04-Aug-2014 |
wenzelm <none@none> |
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
|
#
bced7572 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
c95192c8 |
|
20-Feb-2014 |
wenzelm <none@none> |
tuned signature; tuned message;
|
#
5be0cf66 |
|
10-Feb-2014 |
wenzelm <none@none> |
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: lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))" using [[simp_depth_limit = 1]] apply simp oops
|
#
6b0c03d3 |
|
04-Feb-2014 |
Lars Hupel <lars.hupel@mytum.de> |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state --HG-- extra : amend_source : ecfd76d4e8277199ca35432e0682414689f265fb
|
#
507cb6b6 |
|
17-Jan-2014 |
wenzelm <none@none> |
back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
|
#
69140ebf |
|
17-Jan-2014 |
wenzelm <none@none> |
tuned;
|
#
28d34867 |
|
17-Jan-2014 |
wenzelm <none@none> |
clarified Simplifier diagnostics -- simplified ML; unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);
|
#
523268e2 |
|
15-Jan-2014 |
wenzelm <none@none> |
general notion of auxiliary bounds within context; revert_bounds as part of regular unparse_term; avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);
|
#
cc39ff13 |
|
12-Jan-2014 |
wenzelm <none@none> |
proper context for clear_simpset: preserve dounds, depth; dismantled obsolete debug_bounds/check_bounds;
|
#
66011900 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature;
|
#
db965533 |
|
10-Jan-2014 |
wenzelm <none@none> |
more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
|
#
4019c319 |
|
10-Jan-2014 |
wenzelm <none@none> |
tuned;
|
#
83bef5f0 |
|
01-Jan-2014 |
wenzelm <none@none> |
clarified simplifier context; eliminated Simplifier.global_context;
|
#
47e6e8c3 |
|
31-Dec-2013 |
wenzelm <none@none> |
proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
|
#
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
|
#
65c6de1e |
|
12-Dec-2013 |
wenzelm <none@none> |
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
|
#
f19a8d08 |
|
12-Dec-2013 |
wenzelm <none@none> |
generic trace operations for main steps of Simplifier;
|
#
acb34a00 |
|
12-Dec-2013 |
wenzelm <none@none> |
tuned signature;
|
#
6b30917c |
|
12-Dec-2013 |
wenzelm <none@none> |
tuned whitespace;
|
#
36259e4f |
|
12-Dec-2013 |
wenzelm <none@none> |
tuned whitespace;
|
#
af34ef83 |
|
12-Dec-2013 |
wenzelm <none@none> |
removed dead code -- ctxt is never visible (see also 658fcba35ed7);
|
#
9fb0cf05 |
|
30-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
14801428 |
|
20-May-2013 |
wenzelm <none@none> |
more rigorous check of simplifier context; tuned;
|
#
df857844 |
|
20-May-2013 |
wenzelm <none@none> |
tuned;
|
#
173848be |
|
16-May-2013 |
wenzelm <none@none> |
tuned signature -- depend on context by default;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
4d5f2397 |
|
04-Apr-2013 |
nipkow <none@none> |
removed unnerving (esp in jedit) and pointless warning
|
#
bd19addd |
|
30-Mar-2013 |
wenzelm <none@none> |
amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
|
#
b0bd12e2 |
|
30-Mar-2013 |
wenzelm <none@none> |
more formal cong_name;
|
#
4f9330a5 |
|
29-Sep-2012 |
wenzelm <none@none> |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
#
871b69bc |
|
29-Aug-2012 |
wenzelm <none@none> |
renamed Position.str_of to Position.here;
|
#
14c5ca62 |
|
31-Mar-2012 |
wenzelm <none@none> |
tuned signature;
|
#
8c4cea1d |
|
27-Feb-2012 |
wenzelm <none@none> |
eliminated odd comment from distant past;
|
#
ce167a73 |
|
14-Feb-2012 |
wenzelm <none@none> |
tuned signature;
|
#
2ba20232 |
|
14-Feb-2012 |
wenzelm <none@none> |
eliminated unused rewrite_goal_rule;
|
#
ecb21187 |
|
14-Feb-2012 |
wenzelm <none@none> |
eliminated obsolete aliases;
|
#
1fee9362 |
|
11-Jan-2012 |
wenzelm <none@none> |
more qualified names; more antiquotations;
|
#
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
f44fa063 |
|
23-Nov-2011 |
wenzelm <none@none> |
tuned;
|
#
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
b76f4299 |
|
07-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);
|
#
a309722d |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned signature -- refined terminology;
|
#
4911f028 |
|
08-Aug-2011 |
wenzelm <none@none> |
misc tuning -- eliminated old-fashioned rep_thm;
|
#
a9de3adb |
|
29-Jun-2011 |
wenzelm <none@none> |
tuned signature;
|
#
9c72c6e0 |
|
29-Jun-2011 |
wenzelm <none@none> |
simplified/unified Simplifier.mk_solver;
|
#
1a5a42ee |
|
09-Jun-2011 |
wenzelm <none@none> |
simplified Name.variant -- discontinued builtin fold_map;
|
#
62029f82 |
|
22-Apr-2011 |
wenzelm <none@none> |
tuned signature;
|
#
87db399e |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans; discontinued old-style constrainAbsC; --HG-- rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
#
0a62e9bc |
|
08-Jan-2011 |
wenzelm <none@none> |
tuned;
|
#
3272990d |
|
17-Dec-2010 |
wenzelm <none@none> |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning; --HG-- rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML
|