removed vars_of, concls_of; removed additional rule instantiation argument; proper enumeration of type rules; append possibilities of set and type rules (analogous to elim-intro in 'rule');

declare impE iffD1 iffD2 ad elim of Pure;

removed lookups count; always try headless rules;

added make_thm (sort-of);

added trace_rules, trace;

removed get_cases, get_induct; added find_cases[ST], finde_induct[ST]; proper indexing of types;

removed read_inst', no longer export insts';

fixed typid;

test: use SkipProof.make_thm instead of Thm.assume;

tuned;

HOLogic.dest_concls, InductAttrib.vars_of;

declare impE iffD1 iffD2 as elim of Pure;

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

* Isar/Pure: fixed 'token_translation' command;

added try;

added certify_tyname;

Exported output_symbols.

Removed unnecessary application of Drule.standard.

Fixed erroneous type constraint in token_translation function.

Exported output_with.

Tuned several functions to improve sharing of unchanged subproofs.

added global modes ref;

sane numerals (stage 3): provide generic "1" on all number types;

* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; note that these symbols are unavailable in Proof General / X-Symbol;

fixed numerals;

added tturnstile, TTurnstile;

*** empty log message ***

*** empty log message ***