HOL/record: now includes concrete syntax for record terms;

added Goal, Goalw;

branching_level = 250;

fixed comment;

Removed duplicate list_length_induct

Reordered a few parameters.

Lex

tuned comment;

Reshuffeling, renaming and a few simple corollaries.

fixed translations;

proper thy files;

fixed update syntax;

improved source: state-based; tuned bulk;

added scan_tvar;

added 'space';

Got rid of NAe.delta

HOL/Update

Removed some traces of UNITY

Changed [/] to [:=] and removed actual definition.

New syntax for function update; moved to main HOL directory

misc tuning;

'more' selector; thms: selector_convs, update_convs; tuned;

added nth_update: 'a -> int * 'a list -> 'a list;

tuned msg;

fixed constdefs syntax;

concrete syntax for record terms; defs for update; field types (just abbreviations at the moment); some thms; various of minor improvements;

New behaviour of asm_full_simp_tac.

added CLASIMPSET(') tacticals;

added trfun_names;

added accesses: string -> string list;

minor corrections

Auto_tac: now uses enhanced version of asm_full_simp_tac, Force_tac: replaced fast_tac by best_tac

added finite_dom_map_of and ran_update

added insert_Collect

corrected and updated description of wrapper mechanism (including addss) added documentation of force_tac

*** empty log message ***

"let" is no longer restricted to FOL terms and allows any logical terms

Let.ML and Let.thy had been omitted

fixed simpset(), claset();

moved records data to Tools/record_package.ML; tuned setup;

nontermials;

Theory.require; adapted to new PureThy.add_defs_i, PureThy.add_axioms;

TypedefPackage.add_typedef; RecordPackage.add_record;

Theory.require;

Logic.mk_defpair; adapted to new PureThy.add_defs_i;

Extensible records with structural subtyping in HOL. See Tools/record_package.ML for the actual implementation.

new theory section 'setup';

nonterminals; tuned setup;

package extensible records with structural subtyping in HOL -- still experimental version;

renamed from typedef.ML;

reworked and moved to Tools/record_package.ML;

removed typedef.ML, record.ML; added Tools/typedef_package.ML, Tools/record_package.ML, Record.thy;

renamed to Tools/typedef_package.ML;

adapted to new PureThy.add_axioms_i; Theory.parent_path;

adapted to new PureThy.add_tthmss; Theory.parent_path;

Theory.require; Logic.mk_defpair; adapted to new PureThy.add_defs_i;

adapted to new PureThy.add_axioms;

new theory section 'nonterminals';

adapted to new PureThy.add_defs;

Theory.require;

tuned setup; simp_add_global, simp_del_global, simp_add_local, simp_del_local attributes;

tuned setup;

tuned names of (add_)store_XXX functions; added attributes to add_thms, add_axioms, add_defs functions;

replaced thy_setup by 'setup' section; adapted to new PureThy.add_axioms / PureThy.add_defs; added 'nonterminals' section;

added append;

added none: 'a -> 'a * 'b attribute list; added no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list; added no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list; added applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list);

tuned error msgs;

moved mk_defpair to logic.ML; moved get_def to thm.ML; moved require_thy to theory.ML;

tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;

renamed setup to apply; added add_nonterminals: bstring list -> theory -> theory; added parent_path: theory -> theory; added root_path: theory -> theory; added require: theory -> string -> string -> unit (from section_utils.ML);

adapted to new PureThy.add_axioms_i;

added defaultS: sg -> sort; added full_name_path: sg -> string -> bstring -> string; added add_nonterminals: bstring list -> sg -> sg;

added thm, thms;

*** empty log message ***

new thms, really demos of the final coalgebra theorem

new thms image_0_left, image_Un_left, etc.

new thm mult_lt_mono1

cleanup for split_all_tac as wrapper in claset()

removed wrong comment

added option_map_eq_Some via AddIffs

*** empty log message ***

delsplits, Addsplits, Delsplits.

Renamed expand_const -> split_const

Added conversion of reg.expr. to automata. Renamed expand_const -> split_const.

Renamed expand_const -> split_const.

Added a few lemmas. Renamed expand_const -> split_const.

New proof of apply_equality and new thm Pi_image_cons

improved split_all_tac significantly

improved keyboard modifiers

added ASCII translation of subseteq

tidied; div & mod

*** empty log message ***

added no_syn;

added mk_cond_defpair, mk_defpair;

Modifications due to improved simplifier.

Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.

improved pair_tac to call prune_params_tac afterwards improved the (bad) efficiency of split_all_tac by about 50% split_all_tac is now added to claset() _before_ other safe tactics

split_all_tac is now added to claset() _before_ other safe tactics

made proof of zmult_congruent2 more stable

simplification of explicit theory usage and merges

removed split_all_tac from claset() globally within IOA

made modifications of the simpset() local significantly simplified (and stabilized) proof of is_asig_of_rename

layout improvement

expandshort; new gcd_induct with inbuilt case analysis

Renamed mod_XXX_cancel to mod_XXX_self Included their div_ equivalents

New laws for mod

proving fib(gcd(m,n)) = gcd(fib m, fib n)

fixed comment;

Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct

bug fixes

can prove the empty relation to be WF

Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct