isabelle update_comments;
authorwenzelm
Wed Jun 06 14:22:54 2018 +0200 (11 months ago)
changeset 68397cace81744c61
parent 68396 7433ee1ed7e3
child 68398 194fa3d2d6a4
isabelle update_comments;
src/HOL/Real_Vector_Spaces.thy
src/HOL/Vector_Spaces.thy
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 14:18:31 2018 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 14:22:54 2018 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    apply (force simp add: linear_def real_scaleR_def[abs_def])
     1.5    done
     1.6  
     1.7 -hide_const (open)\<comment>\<open>locale constants\<close>
     1.8 +hide_const (open)\<comment> \<open>locale constants\<close>
     1.9    real_vector.dependent
    1.10    real_vector.independent
    1.11    real_vector.representation
    1.12 @@ -89,7 +89,7 @@
    1.13    unfolding linear_def real_scaleR_def
    1.14    by (rule refl)+
    1.15  
    1.16 -hide_const (open)\<comment>\<open>locale constants\<close>
    1.17 +hide_const (open)\<comment> \<open>locale constants\<close>
    1.18    real_vector.construct
    1.19  
    1.20  lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g o f)"
    1.21 @@ -168,7 +168,7 @@
    1.22    apply (erule (1) nonzero_inverse_scaleR_distrib)
    1.23    done
    1.24  
    1.25 -lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment>\<open>legacy name\<close>
    1.26 +lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
    1.27  
    1.28  named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
    1.29  
     2.1 --- a/src/HOL/Vector_Spaces.thy	Wed Jun 06 14:18:31 2018 +0200
     2.2 +++ b/src/HOL/Vector_Spaces.thy	Wed Jun 06 14:22:54 2018 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4  
     2.5  locale vector_space =
     2.6    fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
     2.7 -  assumes vector_space_assms:\<comment>\<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
     2.8 +  assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
     2.9     allows us to rewrite in the sublocale.\<close>
    2.10      "a *s (x + y) = a *s x + a *s y"
    2.11      "(a + b) *s x = a *s x + b *s x"
    2.12 @@ -68,7 +68,7 @@
    2.13  sublocale module scale rewrites "module_hom = linear"
    2.14    by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+
    2.15  
    2.16 -lemmas\<comment>\<open>from \<open>module\<close>\<close>
    2.17 +lemmas\<comment> \<open>from \<open>module\<close>\<close>
    2.18        linear_id = module_hom_id
    2.19    and linear_ident = module_hom_ident
    2.20    and linear_scale_self = module_hom_scale_self
    2.21 @@ -607,7 +607,7 @@
    2.22  
    2.23  context fixes f assumes "linear s1 s2 f" begin
    2.24  interpretation linear s1 s2 f by fact
    2.25 -lemmas\<comment>\<open>from locale \<open>module_hom\<close>\<close>
    2.26 +lemmas\<comment> \<open>from locale \<open>module_hom\<close>\<close>
    2.27        linear_0 = zero
    2.28    and linear_add = add
    2.29    and linear_scale = scale
    2.30 @@ -634,7 +634,7 @@
    2.31    rewrites "module_hom = linear"
    2.32    by unfold_locales (fact module_hom_eq_linear)
    2.33  
    2.34 -lemmas\<comment>\<open>from locale \<open>module_pair\<close>\<close>
    2.35 +lemmas\<comment> \<open>from locale \<open>module_pair\<close>\<close>
    2.36        linear_eq_on_span = module_hom_eq_on_span
    2.37    and linear_compose_scale_right = module_hom_scale
    2.38    and linear_compose_add = module_hom_add
    2.39 @@ -834,7 +834,7 @@
    2.40    by (auto simp: that construct_in_span in_span_in_range_construct)
    2.41  
    2.42  lemma linear_independent_extend_subspace:
    2.43 -  \<comment>\<open>legacy: use @{term construct} instead\<close>
    2.44 +  \<comment> \<open>legacy: use @{term construct} instead\<close>
    2.45    assumes "vs1.independent B"
    2.46    shows "\<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = vs2.span (f`B)"
    2.47    by (rule exI[where x="construct B f"])