src/HOL/ROOT.ML
Fri, 02 Jul 2010 14:23:17 +0200 haftmann tuned bootstrap files
Tue, 29 Dec 2009 16:20:39 +0100 wenzelm explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
Wed, 11 Nov 2009 14:15:11 +0100 wenzelm uniform use of simultabeous use_thys;
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn processing of tuples in introduction rules
Thu, 26 Feb 2009 22:12:41 +0100 wenzelm back to canonical ROOT, to see if memory problems still persist;
Tue, 27 Jan 2009 12:59:22 +0100 wenzelm added share_common_data -- reduces heap space, but takes long;
Sun, 11 Jan 2009 17:34:02 +0100 wenzelm load main entry points sequentially, for reduced memory demands;
Fri, 02 Jan 2009 00:21:59 +0100 wenzelm tuned header and description of boot files;
Fri, 19 Dec 2008 16:39:23 +0100 ballarin All logics ported to new locales.
Sun, 14 Dec 2008 18:45:51 +0100 ballarin Ported HOL and HOL-Library to new locales.
Fri, 05 Dec 2008 18:42:39 +0100 haftmann corrected theory path
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Wed, 17 Sep 2008 21:27:14 +0200 wenzelm moved global ML bindings to global place;
Tue, 01 Jul 2008 07:58:17 +0200 haftmann HOL += HOL-Complex
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Fri, 25 Jan 2008 14:53:58 +0100 haftmann consistent interacitve bootstrap of HOL-Main
Sat, 21 Jul 2007 23:25:00 +0200 wenzelm tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
Thu, 31 May 2007 18:16:57 +0200 wenzelm proper loading of ML files (in HOL.thy);
Thu, 17 May 2007 19:49:40 +0200 haftmann canonical prefixing of class constants
Sun, 13 May 2007 18:15:21 +0200 haftmann added modules rat.ML and int.ML
Wed, 27 Dec 2006 19:09:58 +0100 haftmann removed Main.thy
Wed, 08 Nov 2006 13:48:35 +0100 wenzelm added structure Main (from Main.ML);
Sun, 11 Jun 2006 00:28:18 +0200 dixon added updated version of IsaPlanner and substitution.
Thu, 02 Mar 2006 18:49:13 +0100 paulson moved the "use" directive
Wed, 01 Mar 2006 06:06:16 +0100 mengj Added file Tools/res_atpset.ML.
Fri, 06 Jan 2006 18:18:13 +0100 wenzelm simplified EqSubst setup;
Sat, 31 Dec 2005 21:49:36 +0100 wenzelm removed obsolete Provers/make_elim.ML;
Thu, 22 Dec 2005 00:29:15 +0100 wenzelm added Provers/project_rule.ML
Wed, 21 Dec 2005 12:06:08 +0100 paulson new hash table module in HOL/Too/s
Fri, 16 Dec 2005 12:15:54 +0100 paulson hashing to eliminate the output of duplicate clauses
Wed, 19 Oct 2005 21:52:31 +0200 wenzelm removed obsolete HOL/thy_syntax.ML;
Fri, 24 Jun 2005 16:21:01 +0200 paulson deleted a redundant "use" line
Mon, 20 Jun 2005 22:13:56 +0200 wenzelm removed obsolete print_depth;
Sun, 22 May 2005 16:51:07 +0200 wenzelm Simplifier already setup in Pure;
Thu, 02 Dec 2004 11:09:19 +0100 paulson new CLAUSIFY attribute for proof reconstruction with lemmas
Wed, 01 Dec 2004 10:14:10 +0100 paulson resolution package tools by Jia Meng
Tue, 03 Aug 2004 14:47:51 +0200 ballarin New transitivity reasoners for transitivity only and quasi orders.
Thu, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Thu, 28 Nov 2002 10:50:42 +0100 ballarin HOL-Algebra partially ported to Isar.
Fri, 23 Aug 2002 07:41:05 +0200 nipkow Added div+mod cancelling simproc
Sun, 21 Jul 2002 15:42:30 +0200 berghofe Added theory for setting up program extraction.
Mon, 22 Oct 2001 11:54:22 +0200 paulson Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
Fri, 19 Oct 2001 22:00:08 +0200 wenzelm got rid of Provers/split_paired_all.ML;
Sun, 14 Oct 2001 22:08:29 +0200 wenzelm moved rulify to ObjectLogic;
Thu, 04 Oct 2001 15:40:52 +0200 wenzelm use "~~/src/Provers/induct_method.ML";
Wed, 03 Jan 2001 11:14:48 +0100 paulson removal of the nat_cancel_factor simproc
Mon, 18 Dec 2000 12:21:54 +0100 paulson loads the new simproc extract_common_term
Wed, 29 Nov 2000 10:19:32 +0100 paulson new simproc file cancel_numeral_factor.ML
Thu, 19 Oct 2000 21:21:41 +0200 wenzelm tuned;
Wed, 18 Oct 2000 23:40:58 +0200 wenzelm path_add "~~/src/HOL/Library";
Thu, 07 Sep 2000 20:50:11 +0200 wenzelm added Provers/rulify;
Wed, 28 Jun 2000 10:37:08 +0200 paulson new file Provers/make_elim.ML
Fri, 05 May 2000 22:25:17 +0200 wenzelm removed Pure/section_utils.ML;
Wed, 03 May 2000 18:34:09 +0200 paulson removed obsolete simproc combine_coeff
Tue, 02 May 2000 18:40:16 +0200 paulson combine_numerals replaces both fold_Suc and combine_coeff
Fri, 21 Apr 2000 11:28:34 +0200 paulson Provers/Arith/inverse_fold.ML is already obsolete
Tue, 18 Apr 2000 15:51:59 +0200 paulson new simprocs for numerals of type "nat"
Tue, 05 Oct 1999 18:16:26 +0200 wenzelm tuned comment;
Mon, 04 Oct 1999 21:45:10 +0200 wenzelm proper dependencies of all theories and packages;
less more (0) -100 -60 tip