meaningful error message on failing merges of coercion tables

add simp rules for enat and ereal

add lemmas

add lemmas

weaken preconditions on lemmas

add lemmas

removing some debug output in quotient_definition

adding quickcheck generators in some HOL-Library theories

adding quickcheck generator for distinct lists; adding examples

added keywords

quickcheck generators for abstract types; tuned

exporting instantiation functions in quickcheck for their usage in abstract generators

generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;

tuned

tuned

ensure TPTP FOF/TFF/THF formulas are close

tuned

merged

added old chestnut

isarfied proof; add log to DERIV_intros

tendsto lemmas for ln and powr

tuned settings;

updated jedit_build component;

updated version information;

patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);

eliminated Drule.export_without_context which is not really required here;

tuned signature;

enforce short hostname on all platforms (especially macbroy2);

clarified modules that contribute to datatype package;

tuned signature;

merged

merged

improved indexed complete lattice

more elementary defs;

eliminated old-fashioned Global_Theory.add_thms(s);

prefer sorting from Scala library;

prefer Name.context operations;

tuned;

clarified modules that contribute to datatype package;

tuned signature;

merged;

tuned;

add complementary lemmas for {min,max}_least

add lemmas about limits

clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

separate rep_datatype.ML; tuned signature;

misc tuning and simplification;

more stats;