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 |