2011-12-20 noschinl 2011-12-20 add simp rules for enat and ereal
2011-12-19 noschinl 2011-12-19 add lemmas
2011-12-19 noschinl 2011-12-19 add lemmas
2011-12-19 noschinl 2011-12-19 weaken preconditions on lemmas
2011-12-19 noschinl 2011-12-19 add lemmas
2011-12-20 bulwahn 2011-12-20 removing some debug output in quotient_definition
2011-12-20 bulwahn 2011-12-20 adding quickcheck generators in some HOL-Library theories
2011-12-20 bulwahn 2011-12-20 adding quickcheck generator for distinct lists; adding examples
2011-12-20 bulwahn 2011-12-20 added keywords
2011-12-20 bulwahn 2011-12-20 quickcheck generators for abstract types; tuned
2011-12-20 bulwahn 2011-12-20 exporting instantiation functions in quickcheck for their usage in abstract generators
2011-12-20 bulwahn 2011-12-20 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;
2011-12-20 bulwahn 2011-12-20 tuned
2011-12-20 bulwahn 2011-12-20 tuned
2011-12-20 blanchet 2011-12-20 ensure TPTP FOF/TFF/THF formulas are close
2011-12-20 nipkow 2011-12-20 tuned
2011-12-19 nipkow 2011-12-19 merged
2011-12-19 nipkow 2011-12-19 added old chestnut
2011-12-19 hoelzl 2011-12-19 isarfied proof; add log to DERIV_intros
2011-12-15 huffman 2011-12-15 tendsto lemmas for ln and powr
2011-12-18 wenzelm 2011-12-18 tuned settings;
2011-12-17 wenzelm 2011-12-17 updated jedit_build component;
2011-12-17 wenzelm 2011-12-17 updated version information;
2011-12-17 wenzelm 2011-12-17 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);
2011-12-17 wenzelm 2011-12-17 eliminated Drule.export_without_context which is not really required here;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-17 wenzelm 2011-12-17 enforce short hostname on all platforms (especially macbroy2);
2011-12-17 wenzelm 2011-12-17 clarified modules that contribute to datatype package;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-16 wenzelm 2011-12-16 merged
2011-12-16 nipkow 2011-12-16 merged
2011-12-16 nipkow 2011-12-16 improved indexed complete lattice
2011-12-16 wenzelm 2011-12-16 more elementary defs;
2011-12-16 wenzelm 2011-12-16 eliminated old-fashioned Global_Theory.add_thms(s);
2011-12-16 wenzelm 2011-12-16 prefer sorting from Scala library;
2011-12-16 wenzelm 2011-12-16 prefer Name.context operations;
2011-12-16 wenzelm 2011-12-16 tuned;
2011-12-16 wenzelm 2011-12-16 clarified modules that contribute to datatype package;
2011-12-16 wenzelm 2011-12-16 tuned signature;
2011-12-15 wenzelm 2011-12-15 merged;
2011-12-15 wenzelm 2011-12-15 tuned;
2011-12-15 noschinl 2011-12-15 add complementary lemmas for {min,max}_least
2011-12-15 noschinl 2011-12-15 add lemmas about limits
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;
2011-12-15 wenzelm 2011-12-15 misc tuning and simplification;
2011-12-15 wenzelm 2011-12-15 more stats;
2011-12-15 blanchet 2011-12-15 made SML/NJ happier
2011-12-15 nipkow 2011-12-15 merged
2011-12-15 nipkow 2011-12-15 tuned
2011-12-15 bulwahn 2011-12-15 hiding the precious name map_entry in AList_Impl
2011-12-14 blanchet 2011-12-14 killed dead code
2011-12-14 blanchet 2011-12-14 use new redirection algorithm in Sledgehammer
2011-12-14 blanchet 2011-12-14 fixed parsing of TPTP atoms
2011-12-14 wenzelm 2011-12-14 tuned signature;
2011-12-14 wenzelm 2011-12-14 avoid fragile Sign.intern_const -- pass internal names directly; tuned;
2011-12-14 wenzelm 2011-12-14 tuned;
2011-12-14 blanchet 2011-12-14 added new proof redirection code
2011-12-14 blanchet 2011-12-14 SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
2011-12-14 blanchet 2011-12-14 make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)