| Tue, 02 Jun 2009 14:37:05 +0200 |
hoelzl |
use algebra_simps instead of ring_simps
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 14:00:24 +0200 |
hoelzl |
Generalized Integral_add
|
file |
diff |
annotate
|
| Fri, 29 May 2009 09:22:56 -0700 |
huffman |
generalize constants from Lim.thy to class metric_space
|
file |
diff |
annotate
|
| Thu, 28 May 2009 22:57:17 -0700 |
huffman |
generalize constants in SEQ.thy to class metric_space
|
file |
diff |
annotate
|
| Tue, 26 May 2009 11:02:59 -0700 |
huffman |
encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
|
file |
diff |
annotate
|
| Tue, 26 May 2009 07:39:52 -0700 |
huffman |
clean up some rsum proofs
|
file |
diff |
annotate
|
| Mon, 25 May 2009 22:14:59 -0700 |
huffman |
use interval sets with gauge predicate
|
file |
diff |
annotate
|
| Mon, 25 May 2009 21:55:07 -0700 |
huffman |
clean up some proofs
|
file |
diff |
annotate
|
| Tue, 24 Feb 2009 11:12:58 -0800 |
huffman |
make more proofs work whether or not One_nat_def is a simp rule
|
file |
diff |
annotate
|
| Sun, 08 Feb 2009 11:59:26 +0100 |
nipkow |
added noatps
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 00:10:58 +0000 |
chaieb |
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 06:55:13 -0800 |
huffman |
Integration imports ATP_Linkup (for metis)
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 11:04:27 -0800 |
huffman |
add lemma psize_unique; simplify some proofs
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 08:31:30 -0800 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|