src/HOL/ROOT.ML
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;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-17 wenzelm 1999-08-17 turned SVC_Oracle into a new-style theory in order to get automatic handling of its additional dependency on Tools/svc_funcs.ML;
1999-08-02 paulson 1999-08-02 new files for the SVC link-up
1999-07-23 paulson 1999-07-23 new simprocs assoc_fold and combine_coeff
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals
1999-07-08 paulson 1999-07-08 new theory IntDiv.thy
1999-07-06 wenzelm 1999-07-06 added Numeral.thy;
1999-04-16 wenzelm 1999-04-16 added Tools/induct_method.ML;
1999-04-14 wenzelm 1999-04-14 Tools/inductive_package.ML;
1999-03-17 wenzelm 1999-03-17 tuned;
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1999-02-08 wenzelm 1999-02-08 ~~;
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-10-20 wenzelm 1998-10-20 split_paired_all.ML;
1998-10-02 paulson 1998-10-02 new file Provers/Arith/abel_cancel.ML
1998-09-25 wenzelm 1998-09-25 tuned;
1998-09-18 paulson 1998-09-18 new files in Integ
1998-09-02 nipkow 1998-09-02 Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
1998-08-12 oheimb 1998-08-12 removed use_thys implied by use_thy "Main"
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-03 wenzelm 1998-07-03 stepping stones: Recdef, Main; String now part of main HOL;
1998-07-02 wenzelm 1998-07-02 fixed Integ;
1998-07-01 berghofe 1998-07-01 Replaced "use_dir" command by "use", because nested calls of "use_dir" cause the HTML generator to crash.
1998-07-01 wenzelm 1998-07-01 tuned Inductive.thy;
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real
1998-05-05 paulson 1998-05-05 New syntax for function update; moved to main HOL directory
1998-04-29 wenzelm 1998-04-29 removed typedef.ML, record.ML; added Tools/typedef_package.ML, Tools/record_package.ML, Record.thy;
1998-03-30 oheimb 1998-03-30 removed superfluous use_thy
1998-01-14 wenzelm 1998-01-14 added record.ML;
1998-01-06 wenzelm 1998-01-06 tuned;