src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
changeset 44165 d26a45f3c835
parent 44142 8e27e0177518
child 44166 d12d89a66742
     1.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 13:24:49 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 09:11:15 2011 -0700
     1.3 @@ -41,9 +41,6 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 -lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
     1.8 -  by auto
     1.9 -
    1.10  lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    1.11    by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
    1.12