src/HOL/ROOT.ML
2009-11-11 wenzelm 2009-11-11 uniform use of simultabeous use_thys;
2009-10-24 bulwahn 2009-10-24 processing of tuples in introduction rules
2009-02-26 wenzelm 2009-02-26 back to canonical ROOT, to see if memory problems still persist;
2009-01-27 wenzelm 2009-01-27 added share_common_data -- reduces heap space, but takes long;
2009-01-11 wenzelm 2009-01-11 load main entry points sequentially, for reduced memory demands;
2009-01-02 wenzelm 2009-01-02 tuned header and description of boot files;
2008-12-19 ballarin 2008-12-19 All logics ported to new locales.
2008-12-14 ballarin 2008-12-14 Ported HOL and HOL-Library to new locales.
2008-12-05 haftmann 2008-12-05 corrected theory path
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-09-17 wenzelm 2008-09-17 moved global ML bindings to global place;
2008-07-01 haftmann 2008-07-01 HOL += HOL-Complex
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-01-25 haftmann 2008-01-25 consistent interacitve bootstrap of HOL-Main
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-05-31 wenzelm 2007-05-31 proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup;
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-13 haftmann 2007-05-13 added modules rat.ML and int.ML
2006-12-27 haftmann 2006-12-27 removed Main.thy
2006-11-08 wenzelm 2006-11-08 added structure Main (from Main.ML);
2006-06-11 dixon 2006-06-11 added updated version of IsaPlanner and substitution.
2006-03-02 paulson 2006-03-02 moved the "use" directive
2006-03-01 mengj 2006-03-01 Added file Tools/res_atpset.ML.
2006-01-06 wenzelm 2006-01-06 simplified EqSubst setup;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-22 wenzelm 2005-12-22 added Provers/project_rule.ML
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-16 paulson 2005-12-16 hashing to eliminate the output of duplicate clauses
2005-10-19 wenzelm 2005-10-19 removed obsolete HOL/thy_syntax.ML;
2005-06-24 paulson 2005-06-24 deleted a redundant "use" line
2005-06-20 wenzelm 2005-06-20 removed obsolete print_depth;
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2004-12-02 paulson 2004-12-02 new CLAUSIFY attribute for proof reconstruction with lemmas
2004-12-01 paulson 2004-12-01 resolution package tools by Jia Meng
2004-08-03 ballarin 2004-08-03 New transitivity reasoners for transitivity only and quasi orders.
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2002-08-23 nipkow 2002-08-23 Added div+mod cancelling simproc
2002-07-21 berghofe 2002-07-21 Added theory for setting up program extraction.
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-19 wenzelm 2001-10-19 got rid of Provers/split_paired_all.ML;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-04 wenzelm 2001-10-04 use "~~/src/Provers/induct_method.ML";
2001-01-03 paulson 2001-01-03 removal of the nat_cancel_factor simproc
2000-12-18 paulson 2000-12-18 loads the new simproc extract_common_term
2000-11-29 paulson 2000-11-29 new simproc file cancel_numeral_factor.ML
2000-10-19 wenzelm 2000-10-19 tuned;
2000-10-18 wenzelm 2000-10-18 path_add "~~/src/HOL/Library";
2000-09-07 wenzelm 2000-09-07 added Provers/rulify;
2000-06-28 paulson 2000-06-28 new file Provers/make_elim.ML
2000-05-05 wenzelm 2000-05-05 removed Pure/section_utils.ML;
2000-05-03 paulson 2000-05-03 removed obsolete simproc combine_coeff
2000-05-02 paulson 2000-05-02 combine_numerals replaces both fold_Suc and combine_coeff
2000-04-21 paulson 2000-04-21 Provers/Arith/inverse_fold.ML is already obsolete
2000-04-18 paulson 2000-04-18 new simprocs for numerals of type "nat"
1999-10-05 wenzelm 1999-10-05 tuned comment;
1999-10-04 wenzelm 1999-10-04 proper dependencies of all theories and packages;
1999-09-21 nipkow 1999-09-21 ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
1999-08-26 wenzelm 1999-08-26 tuned;