added eq_consts; reverted abbrevs: try all abstraction prefixes;

minor tuning of proofs, notably induct;

simplified TableFun.join;

\usepackage{amssymb};

* include generalised MVT in HyperReal (contributed by Benjamin Porter) * add non-denumerability of continuum in Real, includes closed intervals on real (contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)

* moved ThreeDivides from Isar_examples to better suited HOL/ex * moved 2 summation lemmas from ThreeDivides to SetInterval

divisibility by 3 theorem, contributed by Benjamin Porter, #85 in http://www.cs.ru.nl/~freek/100/

replaced mixfix_conflict by mixfix_content;

added map_theory; added rename_frees; removed custom_accesses; added qualified_force_prefix; tuned local syntax;

added abbreviations: activated by init, no expressions yet;

added restore; consts: provide abbreviations;

tuned mixfixes, mixfix_conflict;

removed custom_accesses; added suffixes_prefixes_split, qualified_force_prefix;

added variant_name;

removed custom_accesses; added qualified_force_prefix;

tuned;

added chop (sane version of splitAt); added prefixes, suffixes;

Changed some code due to changes in reduce_axiomsN.ML.

Added another filter strategy.

improved code generator devarification

statement: improved error msg;

* ML/Pure: generic Args/Attrib syntax everywhere;

moved fixedN to lexicon.ML; tuned;

added mfix_delims; tuned;

added mixfix_conflict;

added fixedN, constN;

tuned comment; moved local syntax to local_syntax.ML; common naming (for abbrevs and thms); transfer: merge consts; tuned pretty_term'; added polymorphic -- special case of generalize; added add_abbrevs(_i); read/cert: expand_consts;

tuned comment;

syntax: Context.generic;

Context.generic is canonical state of parsers; removed obsolete global/local parsers; tuned interfaces;

Local syntax depending on theory syntax.

decode: observe Syntax.constN;

removed obsolete add_typ/term_classes/tycons;

tuned extern_term, pretty_term';

removed set quick_and_dirty and ThmDeps.enable -- no effect here;

abbrevs: store in reverted orientation; tuned;

use proof_general.ML: setmp quick_and_dirty captures default value;

added Isar/local_syntax.ML;

tuned;

Args/Attrib syntax: Context.generic;

simplified polyml example;

tidying

blacklist tweaks

names for simprules

removed redundant lemmas

no longer need All_equiv lemmas

map_type_tvar/tfree: map_atyps;

tuned;

*** empty log message ***

made "dvd" on numbers executable by simp.

introduced gen_distinct in place of distinct

fixed the most silly bug conceivable in map_atyps

lambda: base name of Const;

adapted Sign.infer_types; removed obsolete lambda' -- same as Term.lambda;

has_duplicates;

adapted Sign.infer_types;

added local consts component; tuned;

Library.is_equal;

removed obsolete sign_of_cterm; adapted Sign.certify_term;

adapted Sign.infer_types(_simult), Sign.certify_term/prop;

export consts_of; removed const_expansion; pretty_term', infer_types(_simult): separate Consts.T argument; added generic certify; simplified certify_term/prop;

removed eq-polymorphic duplicates; renamed gen_duplicates to duplicates; added is_equal;

renamed space to space_of; removed expansion; added abbrevs_of; added read_const; certify: substitute arguments into expanded const; tuned;

renamed gen_duplicates to duplicates;

slight improvements in code generation

updated;

Logic.combound;

adapted Consts.dest;

Sign.cert_def; tuned;

added bound_vars;

TableFun: renamed xxx_multi to xxx_list; tuned;

Envir.(beta_)eta_contract; TableFun: renamed xxx_multi to xxx_list;

added local_theory, with optional locale xname;

type local_theory; removed _loc versions;

norm_term: Sign.const_expansion, Envir.expand_atom;

TableFun: renamed xxx_multi to xxx_list; tuned LocalDefs.cert_def;

type local_theory = Proof.context; print_consts: subject to quiet_mode;

cert_def: use Logic.dest_def; moved abs_def to logic.ML; derived_def: conditional flag;

Toplevel.local_theory;

LocalDefs.cert_def; tuned;

eq_prop: Envir.beta_eta_contract;

renamed xxx_multi to xxx_list; tuned;

moved combound, rlist_abs to logic.ML;

union_tpairs: Library.merge; Envir.(beta_)eta_contract; tuned;

moved no_vars to sign.ML; removed dest_def (cf. Sign.cert_def);

lambda: abstract over any const; tuned;

added add_abbrevs(_i); moved const_of_class/class_of_const to logic.ML; added no_vars (from theory.ML); added cert_def; added const_expansion; certify: refer to Consts.certify, which includes expansion;

moved (beta_)eta_contract to envir.ML; tuned;

tuned;

added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML);

added (beta_)eta_contract (from pattern.ML); added expand_atom;

print_theory: const abbreviations;

added abbreviations; added certify (mostly from sign.ML);

load envir.ML and logic.ML early;

Logic.rlist_abs;

Logic.const_of_class/class_of_const;

TableFun: renamed xxx_multi to xxx_list;

replaced Symtab.merge_multi by local merge_rules;

Envir.(beta_)eta_contract;

subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate

added strip_abs

clarified semantics of merge

speedup: use simproc for AC rules

UU_reorient_simproc no longer rewrites UU = numeral

removed obsolete gen_ins/mem; added merge -- supercedes gen_merge_lists';

removed add/del_rules;

canonical member/insert/merge;

removal of case analysis clauses

fix

minor improvements

refined signature of locale module

no toplevel 'thy' anymore