| Wed, 12 May 2010 12:31:51 +0200 |
haftmann |
tuned test problems
|
file |
diff |
annotate
|
| Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:40 +0200 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 21:41:05 +0200 |
haftmann |
use code_reflect
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 17:21:48 +0100 |
hoelzl |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:39:51 +0200 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
file |
diff |
annotate
|
| Sat, 20 Jun 2009 13:34:54 +0200 |
nipkow |
added lemmas; tuned
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 16:55:01 -0700 |
huffman |
new GCD library, courtesy of Jeremy Avigad
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 19:36:04 +0100 |
nipkow |
1. New cancellation simprocs for common factors in inequations
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 10:58:18 +0100 |
hoelzl |
Updated paths in Decision_Procs comments and NEWS
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 06:33:48 -0800 |
huffman |
add type annotation
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 11:29:59 -0800 |
huffman |
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
| base
|