src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

 lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
   shows "matrix(adjoint f) = transpose(matrix f)"
   apply (subst matrix_vector_mul[OF lf])
   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
 
-section {* lambda_skolem on cartesian products *}
+section {* lambda skolemization on cartesian products *}
 
 (* FIXME: rename do choice_cart *)
 
 lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
-   (\<exists>x::'a ^ 'n. \<forall>i. P i (x$i))" (is "?lhs \<longleftrightarrow> ?rhs")
+   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   let ?S = "(UNIV :: 'n set)"
   {assume H: "?rhs"
     then have ?lhs by auto}
   moreover
   {assume H: "?lhs"
     then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
     let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
     {fix i
       from f have "P i (f i)" by metis
-      then have "P i (?x$i)" by auto
+      then have "P i (?x $ i)" by auto
     }
     hence "\<forall>i. P i (?x$i)" by metis
     hence ?rhs by metis }
   ultimately show ?thesis by metis
 qed

   show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"]) 
     using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
     unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
 qed
 
-subsection {* Lemmas for working on real^1 *}
+subsection {* Lemmas for working on @{typ "real^1"} *}
 
 lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
   by (metis num1_eq_iff)
 
 lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"