src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
changeset 44142 8e27e0177518
parent 44141 0697c01ff3ea
child 44165 d26a45f3c835
     1.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -42,7 +42,7 @@
     1.4  *}
     1.5  
     1.6  lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
     1.7 -  by (auto intro: ext)
     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)