| Fri, 24 Jun 2005 16:21:01 +0200 |
paulson |
deleted a redundant "use" line
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:13:56 +0200 |
wenzelm |
removed obsolete print_depth;
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:09:19 +0100 |
paulson |
new CLAUSIFY attribute for proof reconstruction with lemmas
|
file |
diff |
annotate
|
| Wed, 01 Dec 2004 10:14:10 +0100 |
paulson |
resolution package tools by Jia Meng
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 14:47:51 +0200 |
ballarin |
New transitivity reasoners for transitivity only and quasi orders.
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:42:30 +0200 |
berghofe |
Added theory for setting up program extraction.
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Fri, 19 Oct 2001 22:00:08 +0200 |
wenzelm |
got rid of Provers/split_paired_all.ML;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:08:29 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:40:52 +0200 |
wenzelm |
use "~~/src/Provers/induct_method.ML";
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 11:14:48 +0100 |
paulson |
removal of the nat_cancel_factor simproc
|
file |
diff |
annotate
|
| Mon, 18 Dec 2000 12:21:54 +0100 |
paulson |
loads the new simproc extract_common_term
|
file |
diff |
annotate
|
| Wed, 29 Nov 2000 10:19:32 +0100 |
paulson |
new simproc file cancel_numeral_factor.ML
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:21:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:40:58 +0200 |
wenzelm |
path_add "~~/src/HOL/Library";
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:50:11 +0200 |
wenzelm |
added Provers/rulify;
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:37:08 +0200 |
paulson |
new file Provers/make_elim.ML
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:25:17 +0200 |
wenzelm |
removed Pure/section_utils.ML;
|
file |
diff |
annotate
|
| Wed, 03 May 2000 18:34:09 +0200 |
paulson |
removed obsolete simproc combine_coeff
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:40:16 +0200 |
paulson |
combine_numerals replaces both fold_Suc and combine_coeff
|
file |
diff |
annotate
|
| Fri, 21 Apr 2000 11:28:34 +0200 |
paulson |
Provers/Arith/inverse_fold.ML is already obsolete
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:51:59 +0200 |
paulson |
new simprocs for numerals of type "nat"
|
file |
diff |
annotate
|
| Tue, 05 Oct 1999 18:16:26 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:45:10 +0200 |
wenzelm |
proper dependencies of all theories and packages;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 14:13:45 +0200 |
nipkow |
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
|
file |
diff |
annotate
|