| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 21:23:42 +0100 |
hoelzl |
int and nat are conditionally_complete_lattices
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:05 +0200 |
hoelzl |
add ceiling_diff_floor_le_1
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 14:09:37 +0200 |
huffman |
add floor/ceiling lemmas suggested by René Thiemann
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 19:28:33 +0200 |
bulwahn |
adding code equations to execute floor and ceiling on rational and real numbers
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 13:41:58 +0200 |
bulwahn |
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 23:33:14 +0200 |
bulwahn |
floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
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, 26 Feb 2009 06:21:31 -0800 |
huffman |
disable floor_minus and ceiling_minus [simp]
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 11:26:01 -0800 |
huffman |
new theory of Archimedean fields
|
file |
diff |
annotate
|