diff -r 7c2404ca7f49 -r 884f54e01427 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Jun 10 19:05:19 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Jun 10 19:10:20 2015 +0200
@@ -1,4 +1,4 @@
-section {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
+section \<open>Instanciates the finite cartesian product of euclidean spaces as a euclidean space.\<close>
 
 theory Cartesian_Euclidean_Space
 imports Finite_Cartesian_Product Integration
@@ -31,7 +31,7 @@
 qed simp
 
 
-subsection{* Basic componentwise operations on vectors. *}
+subsection\<open>Basic componentwise operations on vectors.\<close>
 
 instantiation vec :: (times, finite) times
 begin
@@ -58,7 +58,7 @@
 
 end
 
-text{* The ordering on one-dimensional vectors is linear. *}
+text\<open>The ordering on one-dimensional vectors is linear.\<close>
 
 class cart_one =
   assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
@@ -90,20 +90,20 @@
   show "x \<le> y \<or> y \<le> x" by auto
 qed
 
-text{* Constant Vectors *}
+text\<open>Constant Vectors\<close>
 
 definition "vec x = (\<chi> i. x)"
 
 lemma interval_cbox_cart: "{a::real^'n..b} = cbox a b"
   by (auto simp add: less_eq_vec_def mem_box Basis_vec_def inner_axis)
 
-text{* Also the scalar-vector multiplication. *}
+text\<open>Also the scalar-vector multiplication.\<close>
 
 definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
   where "c *s x = (\<chi> i. c * (x$i))"
 
 
-subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
+subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space.\<close>
 
 lemma setsum_cong_aux:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
@@ -111,7 +111,7 @@
 
 hide_fact (open) setsum_cong_aux
 
-method_setup vector = {*
+method_setup vector = \<open>
 let
   val ss1 =
     simpset_of (put_simpset HOL_basic_ss @{context}
@@ -135,7 +135,7 @@
 in
   Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths))
 end
-*} "lift trivial vector statements to real arith statements"
+\<close> "lift trivial vector statements to real arith statements"
 
 lemma vec_0[simp]: "vec 0 = 0" by vector
 lemma vec_1[simp]: "vec 1 = 1" by vector
@@ -161,7 +161,7 @@
   then show ?case by (auto simp add: vec_add)
 qed
 
-text{* Obvious "component-pushing". *}
+text\<open>Obvious "component-pushing".\<close>
 
 lemma vec_component [simp]: "vec x $ i = x"
   by vector
@@ -180,7 +180,7 @@
   vector_scaleR_component cond_component
 
 
-subsection {* Some frequently useful arithmetic lemmas over vectors. *}
+subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
 
 instance vec :: (semigroup_mult, finite) semigroup_mult
   by default (vector mult.assoc)
@@ -332,9 +332,9 @@
   using setsum_norm_allsubsets_bound[OF assms]
   by simp
 
-subsection {* Matrix operations *}
+subsection \<open>Matrix operations\<close>
 
-text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
+text\<open>Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\<close>
 
 definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
     (infixl "**" 70)
@@ -445,7 +445,7 @@
 lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
   by (metis transpose_transpose rows_transpose)
 
-text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
+text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
 
 lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
   by (simp add: matrix_vector_mult_def inner_vec_def)
@@ -477,7 +477,7 @@
     by simp
 qed
 
-text{* Inverse matrices  (not necessarily square) *}
+text\<open>Inverse matrices  (not necessarily square)\<close>
 
 definition
   "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
@@ -486,7 +486,7 @@
   "matrix_inv(A:: 'a::semiring_1^'n^'m) =
     (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
 
-text{* Correspondence between matrices and linear operators. *}
+text\<open>Correspondence between matrices and linear operators.\<close>
 
 definition matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
   where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
@@ -536,7 +536,7 @@
   done
 
 
-subsection {* lambda skolemization on cartesian products *}
+subsection \<open>lambda skolemization on cartesian products\<close>
 
 (* FIXME: rename do choice_cart *)
 
@@ -736,7 +736,7 @@
   unfolding matrix_right_invertible_span_columns
   ..
 
-text {* The same result in terms of square matrices. *}
+text \<open>The same result in terms of square matrices.\<close>
 
 lemma matrix_left_right_inverse:
   fixes A A' :: "real ^'n^'n"
@@ -765,7 +765,7 @@
   then show ?thesis by blast
 qed
 
-text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *}
+text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
 
 definition "rowvector v = (\<chi> i j. (v$j))"
 
@@ -836,7 +836,7 @@
     obtain l1::"'a^'n" and r1 where r1:"subseq r1"
       and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
       using insert(3) by auto
-    have s': "bounded ((\<lambda>x. x $ k) ` range f)" using `bounded (range f)`
+    have s': "bounded ((\<lambda>x. x $ k) ` range f)" using \<open>bounded (range f)\<close>
       by (auto intro!: bounded_component_cart)
     have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp
     have "bounded (range (\<lambda>i. f (r1 i) $ k))"
@@ -850,9 +850,9 @@
     moreover
     def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
     { fix e :: real assume "e > 0"
-      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
+      from lr1 \<open>e>0\<close> have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
         by blast
-      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially"
+      from lr2 \<open>e>0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially"
         by (rule tendstoD)
       from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
         by (rule eventually_subseq)
@@ -1159,8 +1159,8 @@
   done
 
 
-subsection {* Component of the differential must be zero if it exists at a local
-  maximum or minimum for that corresponding component. *}
+subsection \<open>Component of the differential must be zero if it exists at a local
+  maximum or minimum for that corresponding component.\<close>
 
 lemma differential_zero_maxmin_cart:
   fixes f::"real^'a \<Rightarrow> real^'b"
@@ -1171,7 +1171,7 @@
     vector_cart[of "\<lambda>j. frechet_derivative f (at x) j $ k"]
   by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def)
 
-subsection {* Lemmas for working on @{typ "real^1"} *}
+subsection \<open>Lemmas for working on @{typ "real^1"}\<close>
 
 lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
   by (metis (full_types) num1_eq_iff)
@@ -1233,7 +1233,7 @@
 
 end
 
-subsection{* The collapse of the general concepts to dimension one. *}
+subsection\<open>The collapse of the general concepts to dimension one.\<close>
 
 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
   by (simp add: vec_eq_iff)
@@ -1254,7 +1254,7 @@
   by (auto simp add: norm_real dist_norm)
 
 
-subsection{* Explicit vector construction from lists. *}
+subsection\<open>Explicit vector construction from lists.\<close>
 
 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"