tuned

proper proof body context for Simplifier plugins (solvers, loopers, ...) -- avoid crash due to Subgoal.FOCUS (before e58bc223f46c);

proper table data structure

--HG--
extra : rebase_source : 74bb8ec99405ac13dce51747a70bb95859ed216c

more direct accessors for simpset

regular merge with no historization, in accordance with regular update

--HG--
extra : rebase_source : 6ff04e75725b6899116318ba26adcfc3f80da070

more structural integrity;

clarified signature;

treat simproc results as atomic -- more compact proof terms;

more robust and convenient treatment of implicit context;

clarified signature: more types;

Jenkins: run ocaml_setup

--HG--
extra : amend_source : 5f7c19b527752c7b3910480f59c0ef874d912dea

comments

reorient -> split; documented split

new simp modifier: reorient

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

tuned signature;

clarified signature: prefer proper order operation;

reduced simp_depth_limit

more symbols;

avoid warnings on duplicate rules in the given list;

eliminated unused simproc identifier;

clarified modules -- simplified bootstrap;

simplified simproc programming interfaces;

eliminated pointless cterms;

trim context for persistent storage;

more thorough transfer;

routine check of theory context;

trim context for persistent storage;

more explicit context;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

tuned;

this warning is hardly useful but produces noisy markers in the jedit interface

rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

clarified Drule.gen_all: observe context more carefully;

Thm.cterm_of and Thm.ctyp_of operate on local context;

clarified signature;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

renamed "pairself" to "apply2", in accordance to @{apply 2};

optional proof context for unify operations, for the sake of proper local options;

eliminated former Proof General preferences;

tuned spelling;

more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;

more source positions;

more qualified names;

tuned signature;
tuned message;

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

interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state

--HG--
extra : amend_source : ecfd76d4e8277199ca35432e0682414689f265fb

back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;

tuned;

clarified Simplifier diagnostics -- simplified ML;
unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);

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);

proper context for clear_simpset: preserve dounds, depth;
dismantled obsolete debug_bounds/check_bounds;

tuned signature;

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;

tuned;

clarified simplifier context;
eliminated Simplifier.global_context;

proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;

generic trace operations for main steps of Simplifier;

tuned signature;

tuned whitespace;

tuned whitespace;

removed dead code -- ctxt is never visible (see also 658fcba35ed7);

tuned signature;

more rigorous check of simplifier context;
tuned;

tuned;

tuned signature -- depend on context by default;

simplifier uses proper Proof.context instead of historic type simpset;

removed unnerving (esp in jedit) and pointless warning

amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;

more formal cong_name;

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

renamed Position.str_of to Position.here;

tuned signature;

eliminated odd comment from distant past;

tuned signature;

eliminated unused rewrite_goal_rule;

eliminated obsolete aliases;

more qualified names;
more antiquotations;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

tuned;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);

tuned signature -- refined terminology;

misc tuning -- eliminated old-fashioned rep_thm;

tuned signature;

simplified/unified Simplifier.mk_solver;

simplified Name.variant -- discontinued builtin fold_map;

tuned signature;

modernized structure Proof_Context;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

tuned;

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

--HG--
rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML