src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
Thu, 11 Mar 2010 15:52:34 +0100 haftmann replaced card_def by card_eq_setsum
Mon, 25 Jan 2010 16:56:24 +0100 hoelzl Replaced vec1 and dest_vec1 by abbreviation.
Thu, 07 Jan 2010 18:56:39 +0100 hoelzl finite annotation on cartesian product is now implicit.
Wed, 06 Jan 2010 13:07:30 +0100 himmelma Made finite cartesian products finite
Thu, 19 Nov 2009 11:57:30 +0100 hoelzl Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
Thu, 19 Nov 2009 11:51:37 +0100 hoelzl Renamed vector_less_eq_def to the more usual name vector_le_def.
Tue, 17 Nov 2009 18:52:30 +0100 hoelzl Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
less more (0) tip