| Fri, 02 Mar 2012 09:35:33 +0100 |
bulwahn |
removing finiteness goals
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:09 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 16:57:51 -0700 |
huffman |
speed up extremely slow metis proof of Sup_real_iff
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 16:48:30 -0700 |
huffman |
remove redundant lemma reals_complete2 in favor of complete_real
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Sun, 09 May 2010 17:47:43 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 10:34:02 -0700 |
huffman |
cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:34 +0100 |
haftmann |
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 19:50:45 +0100 |
hoelzl |
Supremum and Infimum on real intervals
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:54 +0100 |
haftmann |
moved auxiliary lemmas to more appropriate places
|
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
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 14:04:56 +0000 |
paulson |
Added two new lemmas
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 11:42:31 +0000 |
paulson |
New theory Probability, which contains a development of measure theory
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 12:59:57 +0000 |
paulson |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
file |
diff |
annotate
|