2010-07-13 ago haftmann canonical argument order for get
2010-07-13 ago haftmann qualified names for (almost) all array operations
2010-07-13 ago haftmann canonical argument order for present
2010-07-13 ago haftmann canonical argument order for length
2010-07-13 ago kleing merged
2010-07-13 ago kleing new crontab
2010-07-13 ago haftmann merged
2010-07-13 ago haftmann proper merge of operation changes and generic do-syntax
2010-07-13 ago haftmann merged
2010-07-13 ago haftmann hide_const; update replaces change
2010-07-13 ago kleing remove separate afp settings again, use plain mac-poly64-M4 instead.
2010-07-13 ago kleing merged
2010-07-13 ago kleing new settings for afp test
2010-07-13 ago krauss Heap_Monad uses Monad_Syntax
2010-07-13 ago krauss State_Monad uses Monad_Syntax
2010-07-13 ago krauss uniform do notation for monads
2010-07-13 ago krauss generic ad-hoc overloading via check/uncheck
2010-07-13 ago haftmann corrected title
2010-07-13 ago haftmann theorem collections do not contain default rules any longer
2010-07-13 ago boehmes fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
2010-07-12 ago wenzelm removed unused/untested IOA 'automaton' package;
2010-07-12 ago wenzelm removed impractical tolerate_legacy_features flag;
2010-07-12 ago wenzelm tuned comment;
2010-07-12 ago wenzelm removed legacy aliases;
2010-07-12 ago wenzelm moved misc legacy stuff from OldGoals to Misc_Legacy;
2010-07-12 ago wenzelm eliminated OldGoals.strip_context;
2010-07-12 ago wenzelm removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
2010-07-12 ago wenzelm do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
2010-07-12 ago wenzelm some modernization of really ancient Meson experiments;
2010-07-12 ago haftmann dropped empty theory
2010-07-12 ago haftmann moved auxiliary lemma
2010-07-12 ago haftmann dropped unused lemmas of dubious value
2010-07-12 ago haftmann dropped unused lemmas of dubious value
2010-07-12 ago haftmann split off mrec into separate theory
2010-07-12 ago haftmann spelt out relational framework in a consistent way
2010-07-12 ago haftmann avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-07-12 ago haftmann merged
2010-07-12 ago haftmann moved co-regularity to class section; avoid duplicated class_deps
2010-07-12 ago haftmann dropped superfluous [code del]s
2010-07-12 ago haftmann merged
2010-07-12 ago haftmann dropped superfluous [code del]s
2010-07-12 ago haftmann more regular session structure
2010-07-10 ago wenzelm 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 ago wenzelm merged
2010-07-09 ago kleing Added current crontab of macbroy28
2010-07-09 ago krauss moved example to its own file in HOL/ex
2010-07-09 ago haftmann merged
2010-07-09 ago haftmann pervasive success combinator
2010-07-09 ago krauss added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
2010-07-09 ago haftmann avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
2010-07-09 ago haftmann adapted to changes
2010-07-09 ago haftmann guard combinator
2010-07-09 ago haftmann tuned reference theory
2010-07-09 ago haftmann tuned array theory
2010-07-09 ago haftmann nicer xsymbol syntax for fcomp and scomp
2010-07-08 ago haftmann dropped ancient in-place compilation of SML; more tests
2010-07-08 ago haftmann updated documentation
2010-07-08 ago haftmann dropped ancient in-place compilation of SML
2010-07-08 ago haftmann more accurate dependencies
2010-07-08 ago haftmann empty default