2006-02-16 obua 2006-02-16 adapted to kernel changes
2006-02-16 wenzelm 2006-02-16 tuned subst_bound(s);
2006-02-15 obua 2006-02-15 fixed bugs, added caching
2006-02-15 wenzelm 2006-02-15 added cases_node; replaced body_context_of by body_context_node, removed no_body_context; copy: ProofContext.transfer; added present_local_theory, present_proof; removed internal command interface;
2006-02-15 wenzelm 2006-02-15 replaced qualified_force_prefix to sticky_prefix; do not export read_terms;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct; replaced qualified_force_prefix by qualified_names/sticky_prefix;
2006-02-15 wenzelm 2006-02-15 check_text: Toplevel.node option;
2006-02-15 wenzelm 2006-02-15 init/exit no longer change the theory (no naming); added naming, restore_naming, mapping;
2006-02-15 wenzelm 2006-02-15 evaluate antiquotes depending on Toplevel.node option;
2006-02-15 wenzelm 2006-02-15 simplified presentation commands;
2006-02-15 wenzelm 2006-02-15 sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
2006-02-15 wenzelm 2006-02-15 removed qualified_force_prefix; added sticky_prefix;
2006-02-15 wenzelm 2006-02-15 replaced qualified_force_prefix to sticky_prefix;
2006-02-15 wenzelm 2006-02-15 chop is no longer pervasive; removed obsolete thms_containing;
2006-02-15 wenzelm 2006-02-15 rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
2006-02-15 wenzelm 2006-02-15 added distinct_prems_rl;
2006-02-15 wenzelm 2006-02-15 specifications_of: avoid partiality;
2006-02-15 wenzelm 2006-02-15 counter example: avoid vacuous trace;
2006-02-15 wenzelm 2006-02-15 cannot use section before setup;
2006-02-15 wenzelm 2006-02-15 used Tactic.distinct_subgoals_tac;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-15 urbanc 2006-02-15 added lemma pt_perm_compose'
2006-02-15 nipkow 2006-02-15 got rid of superfluous linorder_neqE-instance for int.
2006-02-15 webertj 2006-02-15 typo in a comment fixed
2006-02-15 haftmann 2006-02-15 exported some interfaces useful for other code generator approaches
2006-02-15 haftmann 2006-02-15 some fixes
2006-02-15 haftmann 2006-02-15 exported specifications_of
2006-02-14 haftmann 2006-02-14 added theory of executable rational numbers
2006-02-14 haftmann 2006-02-14 improved handling of iml abstractions
2006-02-14 paulson 2006-02-14 fixed tracing
2006-02-13 berghofe 2006-02-13 Adapted to Context.generic syntax.
2006-02-13 mengj 2006-02-13 Fixed a bug of type unification.
2006-02-12 wenzelm 2006-02-12 * ML/Pure/General: improved join interface for tables;
2006-02-12 wenzelm 2006-02-12 consts: maintain thy version for efficient transfer; ins_sorts: Vartab.replace is slower than Vartab.update, but might avoid some copying of table structure;
2006-02-12 wenzelm 2006-02-12 tuned;
2006-02-12 wenzelm 2006-02-12 export exception SAME (for join); join: use internal modify, no option type (handle SAME/DUP instead); defined: simplified copy of lookup code, avoids allocation of option constructor; added replace, which does not change equal entries;
2006-02-12 wenzelm 2006-02-12 low-level tuning of merge: maintain identity of accesses; simplified TableFun.join;
2006-02-12 wenzelm 2006-02-12 share exception UNDEF with Table; simplified TableFun.join;
2006-02-12 wenzelm 2006-02-12 structure Datatab: private copy avoids potential conflict of table exceptions; simplified TableFun.join;
2006-02-12 wenzelm 2006-02-12 added eq_consts; reverted abbrevs: try all abstraction prefixes;
2006-02-12 wenzelm 2006-02-12 minor tuning of proofs, notably induct;
2006-02-12 wenzelm 2006-02-12 simplified TableFun.join;
2006-02-12 wenzelm 2006-02-12 \usepackage{amssymb};
2006-02-12 kleing 2006-02-12 * 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/)
2006-02-12 kleing 2006-02-12 * moved ThreeDivides from Isar_examples to better suited HOL/ex * moved 2 summation lemmas from ThreeDivides to SetInterval
2006-02-12 kleing 2006-02-12 divisibility by 3 theorem, contributed by Benjamin Porter, #85 in http://www.cs.ru.nl/~freek/100/
2006-02-11 wenzelm 2006-02-11 replaced mixfix_conflict by mixfix_content;
2006-02-11 wenzelm 2006-02-11 added map_theory; added rename_frees; removed custom_accesses; added qualified_force_prefix; tuned local syntax;
2006-02-11 wenzelm 2006-02-11 added abbreviations: activated by init, no expressions yet;
2006-02-11 wenzelm 2006-02-11 added restore; consts: provide abbreviations;
2006-02-11 wenzelm 2006-02-11 tuned mixfixes, mixfix_conflict;
2006-02-11 wenzelm 2006-02-11 removed custom_accesses; added suffixes_prefixes_split, qualified_force_prefix;
2006-02-11 wenzelm 2006-02-11 added variant_name;
2006-02-11 wenzelm 2006-02-11 removed custom_accesses; added qualified_force_prefix;
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-11 wenzelm 2006-02-11 added chop (sane version of splitAt); added prefixes, suffixes;
2006-02-11 mengj 2006-02-11 Changed some code due to changes in reduce_axiomsN.ML.
2006-02-11 mengj 2006-02-11 Added another filter strategy.
2006-02-10 haftmann 2006-02-10 improved code generator devarification
2006-02-10 wenzelm 2006-02-10 statement: improved error msg;