diff -r ad6d4a14adb5 -r f03a01a18c6e src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -13,7 +13,7 @@
   "HOL-Library.FuncSet"
 begin
 
-subsection%unimportant \<open>Finite Cartesian products, with indexing and lambdas\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Finite Cartesian products, with indexing and lambdas\<close>
 
 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
@@ -165,7 +165,7 @@
     by (simp add: image_comp o_def vec_nth_inverse)
 qed
 
-subsection%unimportant \<open>Group operations and class instances\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Group operations and class instances\<close>
 
 instantiation vec :: (zero, finite) zero
 begin
@@ -230,7 +230,7 @@
   by standard (simp_all add: vec_eq_iff)
 
 
-subsection%unimportant\<open>Basic componentwise operations on vectors\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic componentwise operations on vectors\<close>
 
 instantiation vec :: (times, finite) times
 begin
@@ -294,15 +294,15 @@
 
 subsection \<open>Real vector space\<close>
 
-instantiation%unimportant vec :: (real_vector, finite) real_vector
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (real_vector, finite) real_vector
 begin
 
-definition%important "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+definition\<^marker>\<open>tag important\<close> "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
 
 lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
   unfolding scaleR_vec_def by simp
 
-instance%unimportant
+instance\<^marker>\<open>tag unimportant\<close>
   by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
 
 end
@@ -310,15 +310,15 @@
 
 subsection \<open>Topological space\<close>
 
-instantiation%unimportant vec :: (topological_space, finite) topological_space
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (topological_space, finite) topological_space
 begin
 
-definition%important [code del]:
+definition\<^marker>\<open>tag important\<close> [code del]:
   "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
     (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
       (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
 
-instance%unimportant proof
+instance\<^marker>\<open>tag unimportant\<close> proof
   show "open (UNIV :: ('a ^ 'b) set)"
     unfolding open_vec_def by auto
 next
@@ -418,7 +418,7 @@
   then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI)
 qed
 
-instance%unimportant vec :: (perfect_space, finite) perfect_space
+instance\<^marker>\<open>tag unimportant\<close> vec :: (perfect_space, finite) perfect_space
 proof
   fix x :: "'a ^ 'b" show "\<not> open {x}"
   proof
@@ -433,29 +433,29 @@
 subsection \<open>Metric space\<close>
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
-instantiation%unimportant vec :: (metric_space, finite) dist
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (metric_space, finite) dist
 begin
 
-definition%important
+definition\<^marker>\<open>tag important\<close>
   "dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV"
 
 instance ..
 end
 
-instantiation%unimportant vec :: (metric_space, finite) uniformity_dist
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (metric_space, finite) uniformity_dist
 begin
 
-definition%important [code del]:
+definition\<^marker>\<open>tag important\<close> [code del]:
   "(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) =
     (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
-instance%unimportant
+instance\<^marker>\<open>tag unimportant\<close>
   by standard (rule uniformity_vec_def)
 end
 
 declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code]
 
-instantiation%unimportant vec :: (metric_space, finite) metric_space
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (metric_space, finite) metric_space
 begin
 
 proposition dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
@@ -557,7 +557,7 @@
   then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
 qed
 
-instance%unimportant vec :: (complete_space, finite) complete_space
+instance\<^marker>\<open>tag unimportant\<close> vec :: (complete_space, finite) complete_space
 proof
   fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
   have "\<And>i. (\<lambda>n. X n $ i) \<longlonglongrightarrow> lim (\<lambda>n. X n $ i)"
@@ -572,14 +572,14 @@
 
 subsection \<open>Normed vector space\<close>
 
-instantiation%unimportant vec :: (real_normed_vector, finite) real_normed_vector
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (real_normed_vector, finite) real_normed_vector
 begin
 
-definition%important "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
+definition\<^marker>\<open>tag important\<close> "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
 
-definition%important "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
+definition\<^marker>\<open>tag important\<close> "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
 
-instance%unimportant proof
+instance\<^marker>\<open>tag unimportant\<close> proof
   fix a :: real and x y :: "'a ^ 'b"
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_vec_def
@@ -609,8 +609,8 @@
   fixes x :: "'a::real_normed_vector^'n"
   assumes "\<And>i. norm(x$i) \<le> norm(y$i)"
   shows "norm x \<le> norm y"
-  unfolding%unimportant norm_vec_def
-  by%unimportant (rule L2_set_mono) (auto simp: assms)
+  unfolding norm_vec_def
+  by (rule L2_set_mono) (auto simp: assms)
 
 lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
   apply (simp add: norm_vec_def)
@@ -638,12 +638,12 @@
 
 subsection \<open>Inner product space\<close>
 
-instantiation%unimportant vec :: (real_inner, finite) real_inner
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (real_inner, finite) real_inner
 begin
 
-definition%important "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"
+definition\<^marker>\<open>tag important\<close> "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"
 
-instance%unimportant proof
+instance\<^marker>\<open>tag unimportant\<close> proof
   fix r :: real and x y z :: "'a ^ 'b"
   show "inner x y = inner y x"
     unfolding inner_vec_def
@@ -672,7 +672,7 @@
 
 text \<open>Vectors pointing along a single axis.\<close>
 
-definition%important "axis k x = (\<chi> i. if i = k then x else 0)"
+definition\<^marker>\<open>tag important\<close> "axis k x = (\<chi> i. if i = k then x else 0)"
 
 lemma axis_nth [simp]: "axis i x $ i = x"
   unfolding axis_def by simp
@@ -696,12 +696,12 @@
 lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
   by (simp add: inner_axis inner_commute)
 
-instantiation%unimportant vec :: (euclidean_space, finite) euclidean_space
+instantiation\<^marker>\<open>tag unimportant\<close> vec :: (euclidean_space, finite) euclidean_space
 begin
 
-definition%important "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
+definition\<^marker>\<open>tag important\<close> "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
 
-instance%unimportant proof
+instance\<^marker>\<open>tag unimportant\<close> proof
   show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
     unfolding Basis_vec_def by simp
 next
@@ -777,7 +777,7 @@
   shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
   by (simp add: axis_eq_axis axis_index_def)
 
-subsection%unimportant \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
 
 lemma sum_cong_aux:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
@@ -851,13 +851,13 @@
 
 lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
 
-lemmas%unimportant vector_component =
+lemmas\<^marker>\<open>tag unimportant\<close> vector_component =
   vec_component vector_add_component vector_mult_component
   vector_smult_component vector_minus_component vector_uminus_component
   vector_scaleR_component cond_component
 
 
-subsection%unimportant \<open>Some frequently useful arithmetic lemmas over vectors\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Some frequently useful arithmetic lemmas over vectors\<close>
 
 instance vec :: (semigroup_mult, finite) semigroup_mult
   by standard (vector mult.assoc)
@@ -996,31 +996,31 @@
 
 text\<open>Matrix notation. NB: an MxN matrix is of type \<^typ>\<open>'a^'n^'m\<close>, not \<^typ>\<open>'a^'m^'n\<close>\<close>
 
-definition%important map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
+definition\<^marker>\<open>tag important\<close> map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
   "map_matrix f x = (\<chi> i j. f (x $ i $ j))"
 
 lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
   by (simp add: map_matrix_def)
 
-definition%important matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
+definition\<^marker>\<open>tag important\<close> matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
     (infixl "**" 70)
   where "m ** m' == (\<chi> i j. sum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
 
-definition%important matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"
+definition\<^marker>\<open>tag important\<close> matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"
     (infixl "*v" 70)
   where "m *v x \<equiv> (\<chi> i. sum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
 
-definition%important vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
+definition\<^marker>\<open>tag important\<close> vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
     (infixl "v*" 70)
   where "v v* m == (\<chi> j. sum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
 
-definition%unimportant "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
-definition%unimportant transpose where
+definition\<^marker>\<open>tag unimportant\<close> "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
+definition\<^marker>\<open>tag unimportant\<close> transpose where
   "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
-definition%unimportant "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
-definition%unimportant "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
-definition%unimportant "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
-definition%unimportant "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
+definition\<^marker>\<open>tag unimportant\<close> "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
+definition\<^marker>\<open>tag unimportant\<close> "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
+definition\<^marker>\<open>tag unimportant\<close> "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
+definition\<^marker>\<open>tag unimportant\<close> "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
 
 lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" 
   by (simp add: matrix_matrix_mult_def zero_vec_def)
@@ -1151,7 +1151,7 @@
 
 text\<open>Correspondence between matrices and linear operators.\<close>
 
-definition%important matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
+definition\<^marker>\<open>tag important\<close> 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)"
 
 lemma matrix_id_mat_1: "matrix id = mat 1"
@@ -1204,10 +1204,10 @@
 
 subsection\<open>Inverse matrices  (not necessarily square)\<close>
 
-definition%important
+definition\<^marker>\<open>tag important\<close>
   "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
 
-definition%important
+definition\<^marker>\<open>tag important\<close>
   "matrix_inv(A:: 'a::semiring_1^'n^'m) =
     (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"