more direct accessors for simpset

clarified signature;

clarified signature;

support for isabelle update -u control_cartouches;

more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
tuned signature;

reorient -> split; documented split

new simp modifier: reorient

clarified signature: prefer proper order operation;

prefer control symbol antiquotations;

more embedded cartouche arguments;
more uniform LaTeX output for control symbols;

more symbols;

provide Pure.simp/simp_all, which only know about meta-equality;

avoid warnings on duplicate rules in the given list;

eliminated unused simproc identifier;

rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

moved remaining display.ML to more_thm.ML;

clarified declaration flags, like 'declaration' command;

simplified simproc programming interfaces;

eliminated pointless cterms;

more uniform "verbose" option to print name space;

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

added Proof_Context.cterm_of/ctyp_of convenience;

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

proper context for assume_tac (atac remains as fall-back without context);

proper context for match_tac etc.;

more explicit Method.modifier with reported position;

added PARALLEL_ALLGOALS convenience;

added simproc markup, which also indicates legacy simprocs outside the name space;

more antiquotations;

tuned signature -- clarified module name;

--HG--
rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML

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

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 signature -- removed obsolete Addsimprocs, Delsimprocs;

added Theory.setup convenience;

less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac;
adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);

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

obsolete -- tools should refer to proper Proof.context;

more formal cong_name;

more item markup;
tuned signature;

Pretty.item markup for improved readability of lists of items;

tuned signature;

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

outermost SELECT_GOAL potentially improves performance;

tuned signature;

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

proper naming of simprocs according to actual target context;
afford pervasive declaration which makes results available with qualified name from outside;

tuned;

tuned signature;

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

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

more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
misc tuning;

tuned -- Variable.declare_term is already part of Variable.auto_fixes;

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

misc tuning -- eliminated old-fashioned rep_thm;

tuned signature;

simplified/unified Simplifier.mk_solver;

ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;

clarified map_simpset versus Simplifier.map_simpset_global;

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

added Name_Space.check/get convenience;

clarified check_simproc (with report) vs. the_simproc;
proper report for @{simproc} (NB: ML environment is built in invisible context);
only one data slot for this module;

proper binding/report of defined simprocs;
tuned signature;

report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;

PARALLEL_GOALS for method "simp_all";

modernized structure Proof_Context;

tuned comment

more explicit references to structure Raw_Simplifier;

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

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

clarified exports of structure Simplifier;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

tuned whitespace

modernized some structure names, keeping a few legacy aliases;

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

export Simplifier.with_context;

conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

proper context for mksimps etc. -- via simpset of the running Simplifier;

eliminated Args.bang_facts (legacy feature);

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

modernized structure Local_Theory;

define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;

adapted Generic_Data, Proof_Data;
tuned;

adapted LocalTheory.declaration;

LocalTheory.naming_of;

make SML/NJ happy;

maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

eliminated dead code;

explicit indication of Unsynchronized.ref;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

modernized method setup;
tuned;

Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;

simplified attribute setup;

eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;

unified type Proof.method and pervasive METHOD combinators;

renamed NameSpace.bind to NameSpace.define;

added dest_ss;
proper context fo pretty_ss;
tuned;

renamed rep_ss to MetaSimplifier.internal_ss;

removed Ids;

dropped NameSpace.declare_base

cleaned up binding module and related code

dropped legacy naming code

namify and name_decl combinators

consider prefixes for name bindings of simprocs (a first approximation)

name/var morphism operates on Name.binding;

ML_Antiquote.value;

proper context for attribute simplified;

Thm.forall_elim_var(s);

purely functional setup of claset/simpset/clasimpset;
tuned signature;

Context.>> : operate on Context.generic;

eliminated delayed theory setup

renamed ML_Context.the_context to ML_Context.the_global_context;

replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

turned simp_depth_limit into configuration option;

added attribute "simproc";
marked some CRITICAL sections;
tuned;

replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;

tuned;

moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);

tuned Pure/General/name_space.ML

simplified DataFun interfaces;

def_simproc(_i): proper ProofContext.read/cert_terms;

canonical merge operations

removed obsolete TypeInfer.logicT -- use dummyT;

exported get_ss, map_ss;

def_simproc(_i): tuned interface;
tuned simprocs environment;

added get_simproc, @{simproc};

added def_simproc(_i) -- define named simprocs;
tuned;

added @{simpset};

moved ML context stuff to from Context to ML_Context;

reorganized structure Tactic vs. MetaSimplifier;

reorganized structure Goal vs. Tactic;

introduces canonical AList functions for loop_tacs

tuned;

Args/Attrib syntax: Context.generic;

simplified type attribute;

setup: theory -> theory;

generic attributes;

Attrib.rule;

export cong_modifiers, simp_modifiers';

added simplification tactics and rules (from meta_simplifier.ML);

renamed set_context to context;
data extend: reset context;

removed obsolete/experimental context components (superceded by Simplifier.the_context);
more abstract change_simpset(_of);
tuned;

export debug_bounds;

export clear_ss;

export MataSimplifier.inherit_bounds;

removed obsolete delta stuff;

multiple flags: prefer later ones;

made smlnj happy;

methods: added simp_flags argument, added "depth_limit" flag;

accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;

moved here from Provers;
removed find_rewrites (superceded by find_theorems rewrite);
outer syntax moved to Pure/Isar/isar_syn.ML;