2010-07-13 krauss 2010-07-13 generic ad-hoc overloading via check/uncheck
2010-07-13 haftmann 2010-07-13 corrected title
2010-07-13 haftmann 2010-07-13 theorem collections do not contain default rules any longer
2010-07-13 boehmes 2010-07-13 fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions; added tests for Ball/Bex
2010-07-12 wenzelm 2010-07-12 removed unused/untested IOA 'automaton' package;
2010-07-12 wenzelm 2010-07-12 removed impractical tolerate_legacy_features flag;
2010-07-12 wenzelm 2010-07-12 tuned comment;
2010-07-12 wenzelm 2010-07-12 removed legacy aliases;
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-07-12 wenzelm 2010-07-12 eliminated OldGoals.strip_context;
2010-07-12 wenzelm 2010-07-12 removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
2010-07-12 wenzelm 2010-07-12 do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel; use up-to-date ML_Compiler.exn_message;
2010-07-12 wenzelm 2010-07-12 some modernization of really ancient Meson experiments;
2010-07-12 haftmann 2010-07-12 dropped empty theory
2010-07-12 haftmann 2010-07-12 moved auxiliary lemma
2010-07-12 haftmann 2010-07-12 dropped unused lemmas of dubious value
2010-07-12 haftmann 2010-07-12 dropped unused lemmas of dubious value
2010-07-12 haftmann 2010-07-12 split off mrec into separate theory
2010-07-12 haftmann 2010-07-12 spelt out relational framework in a consistent way
2010-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-07-12 haftmann 2010-07-12 merged
2010-07-12 haftmann 2010-07-12 moved co-regularity to class section; avoid duplicated class_deps
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-12 haftmann 2010-07-12 merged
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-12 haftmann 2010-07-12 more regular session structure
2010-07-10 wenzelm 2010-07-10 regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;
2010-07-10 wenzelm 2010-07-10 merged
2010-07-09 kleing 2010-07-09 Added current crontab of macbroy28
2010-07-09 krauss 2010-07-09 moved example to its own file in HOL/ex
2010-07-09 haftmann 2010-07-09 merged
2010-07-09 haftmann 2010-07-09 pervasive success combinator
2010-07-09 krauss 2010-07-09 added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
2010-07-09 haftmann 2010-07-09 avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
2010-07-09 haftmann 2010-07-09 adapted to changes
2010-07-09 haftmann 2010-07-09 guard combinator
2010-07-09 haftmann 2010-07-09 tuned reference theory
2010-07-09 haftmann 2010-07-09 tuned array theory
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-07-08 haftmann 2010-07-08 dropped ancient in-place compilation of SML; more tests
2010-07-08 haftmann 2010-07-08 updated documentation
2010-07-08 haftmann 2010-07-08 dropped ancient in-place compilation of SML
2010-07-08 haftmann 2010-07-08 more accurate dependencies
2010-07-08 haftmann 2010-07-08 empty default
2010-07-08 haftmann 2010-07-08 checking generated code for various target languages
2010-07-08 haftmann 2010-07-08 tuned titles
2010-07-08 haftmann 2010-07-08 tuned module names
2010-07-08 haftmann 2010-07-08 tuned tabs
2010-07-08 haftmann 2010-07-08 tuned script
2010-07-08 haftmann 2010-07-08 combinator with_tmp_dir
2010-07-08 haftmann 2010-07-08 rm_tree: remove entire file system trees
2010-07-07 berghofe 2010-07-07 Boxes may now have different widths.
2010-07-07 hoelzl 2010-07-07 tuned
2010-07-07 bulwahn 2010-07-07 replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
2010-07-07 bulwahn 2010-07-07 added NEWS entry
2010-07-07 bulwahn 2010-07-07 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
2010-07-06 huffman 2010-07-06 merged
2010-07-05 huffman 2010-07-05 generalize type of is_interval to class euclidean_space
2010-07-05 huffman 2010-07-05 section -> subsection
2010-07-04 huffman 2010-07-04 generalize some lemmas about derivatives