1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Jun 23 08:44:44 2010 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Jun 23 10:05:13 2010 +0200
1.3 @@ -975,12 +975,12 @@
1.4 apply (subst matrix_vector_mul[OF lf])
1.5 unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
1.6
1.7 -section {* lambda_skolem on cartesian products *}
1.8 +section {* lambda skolemization on cartesian products *}
1.9
1.10 (* FIXME: rename do choice_cart *)
1.11
1.12 lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
1.13 - (\<exists>x::'a ^ 'n. \<forall>i. P i (x$i))" (is "?lhs \<longleftrightarrow> ?rhs")
1.14 + (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
1.15 proof-
1.16 let ?S = "(UNIV :: 'n set)"
1.17 {assume H: "?rhs"
1.18 @@ -991,7 +991,7 @@
1.19 let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
1.20 {fix i
1.21 from f have "P i (f i)" by metis
1.22 - then have "P i (?x$i)" by auto
1.23 + then have "P i (?x $ i)" by auto
1.24 }
1.25 hence "\<forall>i. P i (?x$i)" by metis
1.26 hence ?rhs by metis }
1.27 @@ -1830,7 +1830,7 @@
1.28 unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
1.29 qed
1.30
1.31 -subsection {* Lemmas for working on real^1 *}
1.32 +subsection {* Lemmas for working on @{typ "real^1"} *}
1.33
1.34 lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
1.35 by (metis num1_eq_iff)