# HG changeset patch
# User nipkow
# Date 1536007103 -7200
# Node ID 4824cc40f42e3356399d776f475c2ca67302a620
# Parent  1145b25c53de5259dc012045dd6bba71ac5d0c46
tuned

diff -r 1145b25c53de -r 4824cc40f42e src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 03 20:46:09 2018 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 03 22:38:23 2018 +0200
@@ -31,7 +31,7 @@
   using finite finite_image_set by blast
 
 
-subsection%unimportant \<open>More interesting properties of the norm.\<close>
+subsection%unimportant \<open>More interesting properties of the norm\<close>
 
 notation inner (infix "\<bullet>" 70)
 
@@ -131,7 +131,7 @@
 qed simp
 
 
-subsection \<open>Orthogonality.\<close>
+subsection \<open>Orthogonality\<close>
 
 definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
 
@@ -200,7 +200,7 @@
 qed
 
 
-subsection \<open>Bilinear functions.\<close>
+subsection \<open>Bilinear functions\<close>
 
 definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
 
@@ -256,7 +256,7 @@
 qed
 
 
-subsection \<open>Adjoints.\<close>
+subsection \<open>Adjoints\<close>
 
 definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
 
@@ -658,7 +658,7 @@
   by (metis linear_imp_has_derivative differentiable_def)
 
 
-subsection%unimportant \<open>We continue.\<close>
+subsection%unimportant \<open>We continue\<close>
 
 lemma independent_bound:
   fixes S :: "'a::euclidean_space set"