# HG changeset patch
# User wenzelm
# Date 1528287774 -7200
# Node ID cace81744c61ef2a68a5820acffbc0fc27d6e01d
# Parent  7433ee1ed7e39bef13dfe0127f65ed354da35b7f
isabelle update_comments;

diff -r 7433ee1ed7e3 -r cace81744c61 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 14:18:31 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 14:22:54 2018 +0200
@@ -70,7 +70,7 @@
   apply (force simp add: linear_def real_scaleR_def[abs_def])
   done
 
-hide_const (open)\<comment>\<open>locale constants\<close>
+hide_const (open)\<comment> \<open>locale constants\<close>
   real_vector.dependent
   real_vector.independent
   real_vector.representation
@@ -89,7 +89,7 @@
   unfolding linear_def real_scaleR_def
   by (rule refl)+
 
-hide_const (open)\<comment>\<open>locale constants\<close>
+hide_const (open)\<comment> \<open>locale constants\<close>
   real_vector.construct
 
 lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g o f)"
@@ -168,7 +168,7 @@
   apply (erule (1) nonzero_inverse_scaleR_distrib)
   done
 
-lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment>\<open>legacy name\<close>
+lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
 
 named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
 
diff -r 7433ee1ed7e3 -r cace81744c61 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Wed Jun 06 14:18:31 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy	Wed Jun 06 14:22:54 2018 +0200
@@ -41,7 +41,7 @@
 
 locale vector_space =
   fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
-  assumes vector_space_assms:\<comment>\<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
+  assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
    allows us to rewrite in the sublocale.\<close>
     "a *s (x + y) = a *s x + a *s y"
     "(a + b) *s x = a *s x + b *s x"
@@ -68,7 +68,7 @@
 sublocale module scale rewrites "module_hom = linear"
   by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+
 
-lemmas\<comment>\<open>from \<open>module\<close>\<close>
+lemmas\<comment> \<open>from \<open>module\<close>\<close>
       linear_id = module_hom_id
   and linear_ident = module_hom_ident
   and linear_scale_self = module_hom_scale_self
@@ -607,7 +607,7 @@
 
 context fixes f assumes "linear s1 s2 f" begin
 interpretation linear s1 s2 f by fact
-lemmas\<comment>\<open>from locale \<open>module_hom\<close>\<close>
+lemmas\<comment> \<open>from locale \<open>module_hom\<close>\<close>
       linear_0 = zero
   and linear_add = add
   and linear_scale = scale
@@ -634,7 +634,7 @@
   rewrites "module_hom = linear"
   by unfold_locales (fact module_hom_eq_linear)
 
-lemmas\<comment>\<open>from locale \<open>module_pair\<close>\<close>
+lemmas\<comment> \<open>from locale \<open>module_pair\<close>\<close>
       linear_eq_on_span = module_hom_eq_on_span
   and linear_compose_scale_right = module_hom_scale
   and linear_compose_add = module_hom_add
@@ -834,7 +834,7 @@
   by (auto simp: that construct_in_span in_span_in_range_construct)
 
 lemma linear_independent_extend_subspace:
-  \<comment>\<open>legacy: use @{term construct} instead\<close>
+  \<comment> \<open>legacy: use @{term construct} instead\<close>
   assumes "vs1.independent B"
   shows "\<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = vs2.span (f`B)"
   by (rule exI[where x="construct B f"])