src/HOL/ROOT.ML
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;
Tue, 21 Sep 1999 14:13:45 +0200 nipkow ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
Thu, 26 Aug 1999 19:04:26 +0200 wenzelm tuned;
Wed, 25 Aug 1999 20:49:02 +0200 wenzelm proper bootstrap of HOL theory and packages;
Tue, 17 Aug 1999 22:11:05 +0200 wenzelm turned SVC_Oracle into a new-style theory in order to get automatic
Mon, 02 Aug 1999 11:24:01 +0200 paulson new files for the SVC link-up
Fri, 23 Jul 1999 17:24:48 +0200 paulson new simprocs assoc_fold and combine_coeff
Mon, 19 Jul 1999 15:27:34 +0200 paulson NatBin: binary arithmetic for the naturals
Thu, 08 Jul 1999 13:37:40 +0200 paulson new theory IntDiv.thy
Tue, 06 Jul 1999 21:09:23 +0200 wenzelm added Numeral.thy;
Fri, 16 Apr 1999 14:49:34 +0200 wenzelm added Tools/induct_method.ML;
Wed, 14 Apr 1999 19:07:04 +0200 wenzelm Tools/inductive_package.ML;
Wed, 17 Mar 1999 16:45:53 +0100 wenzelm tuned;
Thu, 11 Mar 1999 13:20:35 +0100 wenzelm removed foo_build_completed -- now handled by session management (via usedir);
Mon, 08 Feb 1999 17:30:22 +0100 wenzelm ~~;
Fri, 27 Nov 1998 17:00:30 +0100 nipkow At last: linear arithmetic for nat!
Tue, 20 Oct 1998 16:39:14 +0200 wenzelm split_paired_all.ML;
Fri, 02 Oct 1998 10:43:08 +0200 paulson new file Provers/Arith/abel_cancel.ML
Fri, 25 Sep 1998 12:12:07 +0200 wenzelm tuned;
Fri, 18 Sep 1998 14:39:51 +0200 paulson new files in Integ
Wed, 02 Sep 1998 16:52:06 +0200 nipkow Added function upto to List.
Wed, 12 Aug 1998 15:38:34 +0200 oheimb removed use_thys implied by use_thy "Main"
Thu, 30 Jul 1998 19:02:52 +0200 wenzelm functorized Clasimp module;
Fri, 24 Jul 1998 13:03:20 +0200 berghofe Adapted to new datatype package.
Fri, 03 Jul 1998 17:35:39 +0200 wenzelm stepping stones: Recdef, Main;
Thu, 02 Jul 1998 16:44:39 +0200 wenzelm fixed Integ;
Wed, 01 Jul 1998 18:43:40 +0200 berghofe Replaced "use_dir" command by "use", because nested calls
Wed, 01 Jul 1998 11:33:39 +0200 wenzelm tuned Inductive.thy;
Tue, 30 Jun 1998 20:42:47 +0200 berghofe Adapted to new inductive definition package.
Thu, 25 Jun 1998 13:57:34 +0200 paulson Installation of target HOL-Real
Tue, 05 May 1998 17:28:22 +0200 paulson New syntax for function update; moved to main HOL directory
Wed, 29 Apr 1998 11:38:52 +0200 wenzelm removed typedef.ML, record.ML;
Mon, 30 Mar 1998 21:04:13 +0200 oheimb removed superfluous use_thy
Wed, 14 Jan 1998 10:32:24 +0100 wenzelm added record.ML;
Tue, 06 Jan 1998 12:32:43 +0100 wenzelm tuned;
less more (0) -60 tip