adding Library theory for other quickcheck default types

removing obsolete ID in Quickcheck_Examples

correcting wellsortedness check and improving error message

using multiple default types in quickcheck

correcting merging of default_types

reordering quickcheck signature; exporting test_params and inspection function

changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types

putting proof in the right context; adding if rewriting; tuned

load_thy: parallel parsing of units, which consist of statement/proof each;

eliminated some unreferenced identifiers;

tuned;

tuned comments;

replaced Source.of_list_limited by slightly more economic Source.of_string_limited;

deps_thy/load_thy: store compact text to reduce space by factor 12;

make SML/NJ happy, by adhoc type-constraints;

recovered benchmarks, which are not tested automatically;

made SML/NJ happy;

merged

abstract visualization of locale ingredients; all_locales yields proper locale identifiers

tuned

accomodate for scope of "as" binding in ML

tuned code

datatype classes are abstract

avoid deprecation

robustified metis proof

modernized abel_cancel simproc setup

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff_minus subsumes diff_def

tuned whitespace