tuned signature;

trim context of persistent data;

more symbols;

"split add" -> "split".
Documented new modifier "split!"

introduced aggressive splitter "split!"

prefer antiquotations;

updated to infer_instantiate;
tuned;

clarified context;

proper context for Object_Logic operations;

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

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

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

eliminated aliases;

modernized setup;

fixed some spelling mistakes

more explicit Method.modifier with reported position;

more qualified names;

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

inst_lift now fully instantiates context to avoid problems with loose bound variables

tuned signature;

tuned signature -- depend on context by default;

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

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

more direct Thm.cprem_of (with exception THM instead of Subscript);
modernized thy;

eliminated old List.nth;
tuned;

modernized structure Object_Logic;

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

standardized filter/filter_out;

eliminated some old folds;

misc tuning and simplification;

uniform use of Integer.min/max;

renamed functor SplitterFun to Splitter, require explicit theory;

explicit OldGoals;

simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;

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

made SML/NJ happy

simplified attribute setup;

simplified method setup;

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

unified type Proof.method and pervasive METHOD combinators;

bug fixes

eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
eliminated obsolete alias rewtac for rewrite_goals_tac;

prove_global: pass context;

Syntax.parse/check/read;

tuned

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;

rep_thm/cterm/ctyp: removed obsolete sign field;

removed obsolete sign_of/sign_of_thm;

switched argument order in *.syntax lifters

simplified method setup;

member (op =);

type annotation added to make SML/NJ happy

linear arithmetic splits certain operators (e.g. min, max, abs)

Args/Attrib syntax: Context.generic;

simplified type attribute;

setup: theory -> theory;

generic attributes;

avoid hardwired Trueprop;
local proof: static refererence to Pure.thy;

renamed Thm.cgoal_of to Thm.cprem_of;

accomodate simplified Thm.lift_rule;

OldGoals;

functor: no Simplifier argument;
change_simpset;

introduced new-style AList operations

use AList operations;

Sign.typ_match;

Move towards standard functions.

Deleted Library.option type.

removed obsolete sort 'logic';

split_name no longer uses Sign.string_of_typ to encode types, since
this depends on the print mode and may lead to unpredictable results.

addsplits / delsplits no longer ignore type of constant.

allowed more general split rules to cope with div/mod 2

CHANGED_PROP;

sar split method uses new gen_split_tac.

Added type constraint in theorem "lift".

Sign.typ_instance;

tuned args;

Args.addN, Args.delN;

tuned msgs;

"split": added "(asm)" option;

added 'split' method;

Now two split thms for same constant at different types is allowed.

use Args.colon / Args.parens;

use Attrib.add_del_args;

made SML/XL happy;

added attributes, method modifiers, theory setup;

- Fixed bug in mk_split_pack which caused application of expansion theorem
to fail because of typing reasons
- Rewrote inst_lift and inst_split: now cterm_instantiate is used to
instantiate theorems

Fixed old bug: selection of constant to be split should depend not just on
the name but also on the type.

renamed mk_meta_eq to mk_eq

added caveat; a real solution would be difficult

the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset

extended addsplits and delsplits to handle also split rules for assumptions
extended const_of_split_thm, renamed it to split_thm_info

Little reorganization. Loop tactics have names now.

adapted to new sort function;

pasted old insertion sort (does not work with new sort function!)

Fixed bug in inst_split.

Tuned function mk_cntxt_splitthm.
Fixed bug which caused split_tac to fail when
(Const ("splitconst", ...) $ ...) was of function type.

renamed split_prem_tac to split_asm_tac
split_asm_tac: simplification, debugged first_prem_is_disj

added split_prem_tac

Added error messages.

fixed dots;

Removal of the tactical STATE

Replaced map...~~ by ListPair.map

Replaced min by Int.min

Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.

Added functions mk_cntxt_splitthm and inst_split which instantiate
the split-rule before it is applied.
Inserted some comments.

Fixed bug.

Completely rewrote split_tac. The old one failed in strange circumstances.

Replaced read by read_cterm.

replaced Pure by ProtoPure

Updated refs to old Sign functions

added header

Initial revision