tuned error handling;

added 'symmetric' attribute;

updated; tuned;

sel_upd proc: include 'more' pseudo-field; added equality rule;

renamed 'mk_cases_tac' to 'ind_cases';

changed 'opaque' option to 'open' (opaque is default); renamed 'mk_cases_tac' to 'ind_cases';

renamed 'RS' to 'THEN'; 'symmetric' attribute;

converted to new-style theory;

done;

'symmetric' attribute;

fixed deps;

renamed 'RS' to 'THEN';

index tokens; added 'int';

cases/induct method: 'opaque' by default; added 'open' option;

updated;

renamed 'RS' to 'THEN'; added 'rename_tac', 'rotate_tac'; added 'subst', 'hypsubst', and 'symmetric';

fixed lbrace, rbrace;

Isar/Pure: renamed 'RS' attribute to 'THEN'; Isar/Provers: added 'arith_split' attribute; Isar/Provers: added 'fastsimp' and 'clarsimp' methods; Isar/HOL/inductive: rename "intrs" to "intros"; HOL/record: added general record equality rule to simpset;

Fixed completeness bug in simplifier: congruence rules could preclude rewrites of the partially applied constant.

major sharpening of stable_project_transient

new (unused) lemma

new thm and simprule Compl_Diff_eq

added conversion.tex;

moved tactic emulation methods here; added print_trans_rules; renamed "res_inst_tac' etc. to 'rule_tac' etc.; added 'fastsimp';

added 'declare' command; moved tactic emulations; tuned; renamed "res_inst_tac' etc. to 'rule_tac' etc.; tuned;

tuned;

updated; tuned;

renamed 'intrs' to 'intros'; updated 'inductive_cases', added 'mk_cases_tac'; 'cases' method: admit multiple insts; added 'arith_split' att;

updated command termination issue;

some more refs;

Aspinall:2000:eProof; Muzalewski:Mizar; Wiedijk:1999:Mizar; Wiedijk:2000:MV;

raplaced "intrs" by "intrs" (new-style only); improved new-style interface to mk_cases;

cases: support multiple insts;

intros;

added MicroJava/BV/StepMono.thy, converted MicroJava/BV/Convert.thy to Isar

Convert.thy now in Isar, tuned

tuned names;

added hypsubst;

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

added declare_theorems(_i); adapted Context.use_let;

added "declare" command;

added thy_script kind;

tuned msg;

use_let: exclude 'val';

fixed document preparation;

documented the integers and updated section on nat arithmetic

some ad-hoc simprules for div and mod to reduce the risk of Suc/number_of clashes

deleted needless rules

added bind_thm for widen_RefT etc.

tuned

added LBV

new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers

ZF arith

interim working version: more improvements to the integers

Equations that are added to the simpset now have proper names.

new structure field "add" for CombineNumerals

the "nocheck" versions of goal functions now standardize their result

tidied

new structure field "add" for CombineNumerals

installation of cancellation simprocs for the integers

X-Symbol mode -- look in canonical place;

fixed spelling;

added Bauer-Wenzel:2000:HB;

thms closure;

res_inst: include non-inst versions with multiple thms; ML tactic: thms closure; tuned msgs;

added get_thms_closure, single_thm;

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

fixed mk_cases_i: TRYALL InductMethod.simp_case_tac;

thms "atomize";

tuned;

tuned

token translation: enclose "\\mbox{" "}";

added Example

moved Hoare_example to Examples; other minor improvements

Deleted unneeded proof; simplified proof of app_last.

added forall_elim_vars_safe, norm_hhf_eq;

norm_hhf results;

prf_heading kind;

MicroJava structure changed

Invoke instruction gets fully qualified method name (class+name+sig) as in Sun's JVM spec

BV and LBV specified in terms of app and step functions

instantiated Cancel_Numerals for "nat" in ZF

more cterm operations: mk_implies, list_implies

prove_conv gets an extra argument, so the ZF instantiation can use hyps

tidied

added a dummy "thm list" argument to prove_conv for the new interface to Cancel_Numerals

new abstract syntax operations, used in ZF

ZF arith

*** empty log message ***

dummy_patterns moved to term.ML;

added goal_args('); added "cut_tac", "thin_tac", "rename_tac"; renamed inst tactics; inst syntax: include empty inst;

added int;

axioms: Term.no_dummy_patterns;

added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;

added rename_params_tac;

dummy_pattern moved to term.ML;

Term.no_dummy_patterns;

added rev_eq_reflection; export stac; proof method setup: subst, hypsubst;

val rev_eq_reflection = def_imp_eq;

val atomize = thms "atomize";

lemmas atomize = all_eq imp_eq; setup hypsubst_setup;

rev_eq_reflection = meta_eq_to_obj_eq;

removed stac (now exported by HypsubstFun);

setup hypsubst_setup;

lemmas atomize = all_eq imp_eq;

added rev_eq_reflection;

subgoals_tac: fixed spelling;

invoke isatool make in any dir containing an IsaMakefile;

updated;

targets for images, test, all;

updated;

tuned;

tuned version by Stephan Merz (unbatchified etc.);

tuned TLA;

added setmp_verbose;

tuned;

unknown_theory/proof/context;

added unknown_theory/proof/context;

new theorem neq_commute

new files Integ/IntPower.{thy.ML}; tidied