| Fri, 05 Mar 2010 10:42:13 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Thu, 04 Mar 2010 21:52:26 +0100 |
hoelzl |
Add Lebesgue integral and probability space.
|
changeset |
files
|
| Thu, 04 Mar 2010 19:50:45 +0100 |
hoelzl |
Supremum and Infimum on real intervals
|
changeset |
files
|
| Thu, 04 Mar 2010 19:43:51 +0100 |
hoelzl |
Rewrite rules for images of minus of intervals
|
changeset |
files
|
| Thu, 04 Mar 2010 18:42:39 +0100 |
hoelzl |
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
|
changeset |
files
|
| Thu, 04 Mar 2010 17:28:45 +0100 |
hoelzl |
Added natfloor and floor rules for multiplication and power.
|
changeset |
files
|
| Thu, 04 Mar 2010 17:09:44 +0100 |
hoelzl |
Generalized setsum_cases
|
changeset |
files
|
| Thu, 04 Mar 2010 15:44:06 +0100 |
hoelzl |
Added vimage_inter_cong
|
changeset |
files
|
| Thu, 04 Mar 2010 18:18:52 -0800 |
huffman |
merged
|
changeset |
files
|
| Thu, 04 Mar 2010 10:01:39 -0800 |
huffman |
move coinduction-related stuff into function prove_coindunction
|
changeset |
files
|
| Thu, 04 Mar 2010 08:12:39 -0800 |
huffman |
add function add_qualified_simp_thm
|
changeset |
files
|
| Wed, 03 Mar 2010 21:42:42 -0800 |
huffman |
generate lemma take_below, declare chain_take [simp]
|
changeset |
files
|