Wed, 13 Nov 2013 09:37:00 +0100 |
hoelzl |
fix document generation for HOL-Probability
|
changeset |
files
|
Tue, 12 Nov 2013 20:08:29 +0100 |
hoelzl |
fix document generation for Extended_Nat
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:56 +0100 |
hoelzl |
measure of a countable union
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:56 +0100 |
hoelzl |
add restrict_space measure
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:55 +0100 |
hoelzl |
better support for enat and ereal conversions
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:55 +0100 |
hoelzl |
enat is countable
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:54 +0100 |
hoelzl |
add equalities for SUP and INF over constant functions
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:54 +0100 |
hoelzl |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:53 +0100 |
hoelzl |
add acyclicI_order
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:52 +0100 |
hoelzl |
stronger inc_induct and dec_induct
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:51 +0100 |
hoelzl |
countability of the image of a reflexive transitive closure
|
changeset |
files
|
Tue, 12 Nov 2013 19:28:51 +0100 |
hoelzl |
support of_rat with 0 or 1 on order relations
|
changeset |
files
|