# 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)\\locale constants\ +hide_const (open)\ \locale constants\ 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)\\locale constants\ +hide_const (open)\ \locale constants\ real_vector.construct lemma linear_compose: "linear f \ linear g \ 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\\legacy name\ +lemmas sum_constant_scaleR = real_vector.sum_constant_scale\ \legacy name\ 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 \ 'b::ab_group_add \ 'b" (infixr "*s" 75) - assumes vector_space_assms:\\re-stating the assumptions of \module\ instead of extending \module\ + assumes vector_space_assms:\ \re-stating the assumptions of \module\ instead of extending \module\ allows us to rewrite in the sublocale.\ "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\\from \module\\ +lemmas\ \from \module\\ 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\\from locale \module_hom\\ +lemmas\ \from locale \module_hom\\ 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\\from locale \module_pair\\ +lemmas\ \from locale \module_pair\\ 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: - \\legacy: use @{term construct} instead\ + \ \legacy: use @{term construct} instead\ assumes "vs1.independent B" shows "\g. linear s1 s2 g \ (\x\B. g x = f x) \ range g = vs2.span (f`B)" by (rule exI[where x="construct B f"])