isabelle update -u control_cartouches;

tuned signature;

more symbols;

removed old proof method "default";

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

tuned signature;

moved remaining display.ML to more_thm.ML;

trim context for persistent storage;

store result of swapify, to avoid later access to implicit context;

trim context for persistent storage;

delete precisely the added rules;
tuned;

clarified context;

tuned whitespace;

tuned signature;

tuned;

clarified context;

prefer tactics with explicit context;

clarified context;

no arguments for "standard" (or old "default") methods;

renamed "default" to "standard", to make semantically clear what it is;

discontinued pointless warnings: commands are only defined inside a theory context;

proper context for Object_Logic operations;

@{command_spec} is superseded by @{command_keyword};

tuned signature -- prefer qualified names;

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

proper context for "net" tactics;
avoid implicit Tactic.build_net -- make its operational behavior explicit in application;

tuned spelling;

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

proper context;

proper context for match_tac etc.;

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

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

eliminated aliases;

modernized setup;

more explicit Method.modifier with reported position;

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

some shortcuts for chunks, which sometimes avoid bulky string output;

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

standardized aliases;

tuned signature;

actually use Data.sizef, not hardwired size_of_thm;

uniform Proof.context for hyp_subst_tac;

tuned signature;

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

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

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

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;

more item markup;
tuned signature;

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

tuned -- eliminate pointless ML method definition;

method setup for Classical steps;

more concise/precise documentation;

--HG--
extra : rebase_source : c44f7ed1dd39b1ed8a453b7e303db9cbcd5921e7

prefer direct rotate_prems over old-style COMP;

outer syntax command definitions based on formal command_spec derived from theory header declarations;

tuned signature;

eliminated obsolete aliases;

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

tuned;

tuned signature;

slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;

more precise warnings: observe context visibility;

modernized functor names;
tuned;

method "deepen" with optional limit;

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

do not open ML structures;

eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);

misc tuning and simplification;

eliminated Display.string_of_thm_without_context;
tuned whitespace;

modernized structure Proof_Context;

clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);

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

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

proper context for rule_by_tactic;

modernized structure Object_Logic;

eliminated Args.bang_facts (legacy feature);

adapted Theory_Data;
tuned;

adapted Generic_Data, Proof_Data;
tuned;

modernized structure Context_Rules;

eliminated some old folds;

standardized filter/filter_out;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

eliminated dead code;
tuned;

eliminated dead code and redundant parameters;
tuned;

explicit indication of Unsynchronized.ref;

removed old global get_claset/map_claset;
added local get_claset/put_claset;

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

structure Thm: less pervasive names;

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

renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);

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;

use exists_subterm directly;

tuned comments;

structure Display: less pervasive operations;

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

unfold_locales now part of default tactic

renamed ML_Context.the_context to ML_Context.the_global_context;

pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;

simplified interfaces for outer syntax;

tuned merge operations via pointer_eq;

ClassPackage renamed to Class

added get_cs/map_cs;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
added flat_rule filter for addXXs etc.;

simplified/unified list fold;

simplified DataFun interfaces;

canonical merge operations

fixed slip

moved Output.overwrite_warn here

moved eq_thm etc. to structure Thm in Pure/more_thm.ML;

moved ML context stuff to from Context to ML_Context;

removed obsolete name_hint handling;

Removal of theorem tagging, which the ATP linkup no longer requires,

reorganized structure Goal vs. Tactic;

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

ProofContext.init;

Toplevel: generic_theory;

Drule.equiv_thm supercedes Drule.weak_eq_thm;

ObjectLogic.is_elim;

moved intro_classes from AxClass to ClassPackage

tuned;

default rule step: norm_hhf_tac;

simplified type attribute;

setup: theory -> theory;

attributes: optional weight;
tuned;

generic attributes;

generic attributes;

store_thm: transfer to current context, i.e. the target theory;

preservation of names

Provers/classical: stricter checks to ensure that supplied intro, dest and
elim rules are well-formed

added classical_rule, which replaces Data.make_elim;
removed obsolete Data.make_elim and classical elim_format attribute;
tuned;

swap: no longer pervasive;

Drule.multi_resolves;

Added "deepen" method.

change_claset(_of): more abtract interface;
claset_of: init proof context;
added raw get_claset;

minor tweaks for Poplog/PML;

introduced binding priority 1 for linear combinators etc.

classical rules must have names for ATP integration

OuterKeyword;

removed obsolete delta stuff;

accomodate change of TheoryDataFun;

Removed most of the atp interface from Pure.

*** MESSAGE REFERS TO PREVIOUS VERSION ***
Method.src;

*** empty log message ***

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

Jia Meng: delta simpsets and clasets

context dependent components;

'instance' and intro_classes now handle general sorts;

dup_elim: improved error reporting;

use eq_thm_prop instead of slightly inadequate eq_thm;

added 'swapped' attribute;
tuned xtra_netpair;
tuned;

simplified (and clarified) integration with Pure/ContextRules;
removed "extra" rules as separate slots, only keep xtra_netpair for
single-step view of plain haz/safe rules;

made SML/NJ happy;

theory data: removed obsolete finish method;

theory data: finish method;

Method.trace ctxt;

Tactic.orderlist;

ObjectLogic.atomize_tac;

moved trace_rules to Pure/Isar/method.ML;
some_rule_tac: prefer Method.some_rule_tac of Pure, no special
handling of imp_elim;

renamed addaltern to addafter, addSaltern to addSafter

corrected comments on addbefore and addSbefore

CHANGED_PROP;

recover_order for single step tules;

tuned method "rule" and "default";

atomize: all automated tactics that "solve" goals;

intro_classes by default;

fixed 'clarify': CHANGED;

tuned args;

Args.addN, Args.delN;

renamed atts: rulify to rule_format, elimify to elim_format;

delrule: handle dest rules as well;
replaced "delrule" by "rule del";

tuned att names / msgs;

added "slow";

added "safe" method;

improved messages;

*** empty log message ***

fixed classification of rules in atts and modifiers (final!?);

unknown_theory/proof/context;

intro_elim_tac: bimatch_from;

added clarify method;
removed unofficial improper methods;

classical atts now intro! / intro / intro?;

strengthened force_tac by using new first_best_tac

classical 'elimify' attribute;

uses a supplied version of make_elim for addDs

Toplevel.no_timing;

improved warning messages;

Pretty.chunks;

intro/elim_tac: match only;

HEADGOAL;

print_simpset / print_claset command;

tuned comments;

tuned comments;

fixed section syntax;

REPEAT_ALL_NEW;

intro/elim/dest attributes: changed ! / !! flags to ? / ??;

HEADGOAL;

replaced FIRSTGOAL by FINDGOAL (backtracking!);

METHOD_CLASET': refer to *local* claset;

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

Method.insert_tac;
Method.multi_resolves;
contradiction: made faithful;
tuned comments;

proper setup of GlobalClaset data;

fixed intro_elim_tac;

intro/elim: REPEAT1;

renamed 'some_rule' to 'rule';

Method.modifier;

renamed 'single' to 'some_rule';
added 'intro', 'elim';

export cla_meth(');

eliminated METHOD0 in favour of same_tac;

safe_step_tac / step_tac;

tuned contradiction method;
improved comments;

dup_elim: use try to handle general exn;

type claset: added extra I/E rules;

theory data: copy;

improved 'single' method;
added 'contradiction' method;

oops;

single method: include not_elim, imp_elim;

cleaned comments;

Theory.sign_of;

eliminated tthm type and Attribute structure;

expoer cla_method('), cla_modifiers;

tuned attribute names;
all modifiers turned into attributes;
realistic method syntax;

local claset theory data;
intro, elim, dest, del attributes;
single_tac and method;
fast, best etc. methods;

corrected (and simplified) depth_tac

added addD2, addE2, addSD2, and addSE2
improved addbefore and addSbefore
improved mechanism for unsafe wrappers

Context.the_context;

accomodate tuned version of theory data;

tuned setup;

type_error;

replaced thy_data by setup;

tuned names;

introduced functions for updating the wrapper lists
merge_cs now uses merge_alists to merge wrapper lists, left cs has precedence!

merge_cs now also merges safe and unsafe wrappers

improved coding of delWrapper and delSWrapper

renamed rep_claset to rep_cs

changed wrapper mechanism of classical reasoner

Catches bad elim rules, handling exception OPTION

oops;

tuned print_cs;

More deterministic (?) contr_tac

added print_claset;

changed Pure/Sequence interface -- isatool fixseq;

adapted print methods;

type object = exn (enhance readability);

new implicit claset mechanism based on Sign.sg anytype data;
tuned warnings;

Fixed comments

Added Safe_tac; all other default claset tactics now dereference "claset"
only when given the proof state

Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac

improved print_cs;

Removal of the tactical STATE

corrected depth_tac: no call for safe_step_tac if subgoal not present

New DEEPEN allows giving an upper bound for deepen_tac

delrules now deletes ALL occurrences of a rule, since it may appear in any of
the four lists.

dup_intr & dup_elim no longer call standard -- this
lets them be used on meta-hyps

moved THEN_MAYBE to Pure/tctical.ML
better addbefore, addafter (now: addaltern),
setwrapper (now: setWrapper) and addwrapper (now addWrapper)
added safe wrapper(and functions setSWrapper,compSWrapper,addSbefore,addSaltern)

Added a comment

Introduction of Slow_tac and Slow_best_tac

Now deepen_tac can take advantage of wrappers --
including addss...

New classical reasoner: warns of, and ignores, redundant rules.
Also warns of rules supplied with different "hints" (Safe, etc.)

Addition of Safe_step_tac

Now exports Delrules

Now implements delrules

Added functions for default claset.

Provides merge_cs to support default clasets

Now provides astar versions (thanks to Norbert Voelker)

imp_elim and swap are now stored in thm database

clarified comment

Recoded addSIs, etc., so that nets are built incrementally
instead of from scratch each time. The old approach used excessive time (>1
sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset
includes all record fields. joinrules no longer sorts the rules on number of
subgoals, since it does not see the full set of them; instead the number of
subgoals modifies the priority.

Added comment.

Addition of wrappers for integration with the simplifier.
New infixes setwrapper compwrapper addbefore addafter. New function
getwrapper. The wrapper is a tactical that is applied to the step tactic. By
default it is the identity. Using THEN one can cause other tactics to be
tried before or after the step tactic. Other effects are possible using
ORELSE, etc.

deepen_tac: modified due to outcome of experiments. Its
choice of unsafe rule to expand is still non-deterministic.

Provers/classical: now takes theorem "classical" as argument, proves "swap"
Provers/classical/depth_tac,deepen_tac: new

chain_tac: deleted; just use etac mp

classical/swap_res_tac: recoded to allow backtracking

Initial revision