updated to latest versions of ttbox and ttbreak

updated;

updated;

updated;

tuned translations;

*** empty log message ***

added \isastyleminor; more \isachars; added \isadigit; improved \isakeyword; tuned;

more \isachars; added \isadigit; simplified command markup;

fixed has_meta_prems: strip_assums_hyp;

*** empty log message ***

updated;

open cases;

output \isachar;

cond_add_path;

fixed text;

turned into new-style theory;

tuned;

tuned \isastyle;

added \isachar definitions; added \isabellestyle switch; tuned;

%\urlstyle{rm} %\isabellestyle{it}

renamed cond_with_path to cond_add_path (add to front); improved with_path(s) (add to rear);

X-symbols for ordinal, cardinal, integer arithmetic

fixed RuleCases.make (invert flag);

removed obsolete add_recdef_x;

proper handling of defs;

Main now new-style theory; added Main.ML for compatibility;

simproc bug fix: only TYPING assumptions are given to the simplifier

better rules for cancellation of common factors across comparisons

new example ZF/ex/NatSum

now allows dest_coeff to fail

*** empty log message ***

*** empty log message ***

removed obsolete keyword;

fixed indexing;

tuned;

installed recdef congs data

added map_cong to recdef

removed Lambda/Type.ML;

better rules for cancellation of common factors across comparisons

fixed a proof that had stopped working ???

tidied & updated proofs, deleting some unused ones

modified proofs: better rules for cancellation of common factors across comparisons

better rules for cancellation of common factors across comparisons

*** empty log message ***

cases: opaque by default; fixed ML tactic: proper context; added 'rename_tac', 'rename_tac';

renamed 'RS' to 'THEN';

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