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 |