author wenzelm Wed Jun 06 14:22:54 2018 +0200 (11 months ago) changeset 68397 cace81744c61 parent 68396 7433ee1ed7e3 child 68398 194fa3d2d6a4
 src/HOL/Real_Vector_Spaces.thy file | annotate | diff | revisions src/HOL/Vector_Spaces.thy file | annotate | diff | revisions
```     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.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