more symbols;

tuned signature;

tuned;

tuned signature -- prefer qualified names;

modernized setup;

more explicit Method.modifier with reported position;

added PARALLEL_ALLGOALS convenience;

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

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

modifiers for classical wrappers operate on Proof.context instead of claset;

tuned;

tuned signature;

discontinued obsolete method fastsimp / tactic fast_simp_tac;

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

new fastforce replacing fastsimp - less confusing name

clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac;
tuned blast_tac: atomize prems only once, outside DEEPEN;

discontinued old / unused addss' (cf. 57f364d1d3b2);

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

simplified clasimpset declarations -- prefer attributes;

tuned;

modernized Clasimp setup;

PARALLEL_GOALS for simplification within auto_tac;

Unification (flexflex) bug fix; making "auto" deterministic

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

eliminated Args.bang_facts (legacy feature);

modernized structure Context_Rules;

eliminated dead code;

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

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

simplified method setup;

simplified attribute setup;

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

unified type Proof.method and pervasive METHOD combinators;

Merge.

use long names for old-style fold combinators;

unified Args.T with OuterLex.token, renamed some operations;

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

renamed ML_Context.the_context to ML_Context.the_global_context;

moved ML context stuff to from Context to ML_Context;

removed obsolete name_hint handling;

removed use of put_name_hint, as the ATP linkup no longer needs this

thm/prf: separate official name vs. additional tags;

simplified type attribute;

setup: theory -> theory;

generic attributes;

generic attributes;
added low-level modifiers from Pure/context_rules.ML;

removed obsolete Provers/make_elim.ML;

modified suffix for [iff] attribute

functor: no Simplifier argument;
export change_clasimpset;

classical rules must have names for ATP integration

Simplifier already setup in Pure;

Move towards standard functions.

Deleted Library.option type.

local_cla/simpset_of;

Merged in license change from Isabelle2004

Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.

iff: conditional rules declared as ``unsafe'';

iff?: refer to Pure/ContextRules;

iff: always rotate prems;

corrected semantics of [iff] concerning rules with premises

removed the warning from [iff]

streamlined addIffs/delIffs, added warnings

renamed addaltern to addafter, addSaltern to addSafter

CHANGED_PROP;

added clasimpset: unit -> clasimpset;

made SML/NJ happy;

added iff_add_global', iff_add_local' (syntax "iff?");
tuned;

Args.addN, Args.delN;

tuned msg;

added 'iff' declarations;

added "slowsimp", "bestsimp";

auto method: opt args;
tuned;

added "fastsimp";
fixed "clarsimp": CHANGED;

export get_local_clasimpset, clasimp_modifiers;

added clarsimp method;

strengthened force_tac by using new first_best_tac

added change_global/local_css;

include Splitter.split_modifiers;

HEADGOAL;

replaced FIRSTGOAL by FINDGOAL (backtracking!);

clarsimp_tac now copes with the (unwanted) case that the simplifier splits
the goal

setup for refined facts handling;
Method.bang_sectioned_args / Args.bang_facts;

renamed improper method 'clarsimp' to 'clarsimp_tac';

Method.insert_tac;

auto: CHANGED;

Method.modifier;

tuned;

eliminated METHOD0 in favour of same_tac;

method brute_force = ALLGOALS force_tac;

method setup;

corrected auto_tac (applications of unsafe wrappers)
by correcting (and simplifying) nodup_depth_tac

deleted illegal "op"

removed addcongs2 and delcongs2
simplified CLASIMP_DATA

improved addbefore and addSbefore
improved mechanism for unsafe wrappers

added clarsimp_tac and Clarsimp_tac

functorized Clasimp module;

added CLASIMPSET(') tacticals;

Auto_tac: now uses enhanced version of asm_full_simp_tac,
Force_tac: replaced fast_tac by best_tac

renamed smart_tac to force_tac, slight improvement of force_tac

added smart_tac

factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML
explicitly introducing combined type clasimpset