# HG changeset patch
# User hoelzl
# Date 1277280313 -7200
# Node ID 6e9f48cf6adf09bd552afa2544c99a1a49976ced
# Parent  2377d246a631114aeeae0f1d64c1c3068f373025
Make latex happy

diff -r 2377d246a631 -r 6e9f48cf6adf src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Jun 23 08:44:44 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Jun 23 10:05:13 2010 +0200
@@ -975,12 +975,12 @@
   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"
@@ -991,7 +991,7 @@
     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 }
@@ -1830,7 +1830,7 @@
     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)