# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530544803 -3600
# Node ID 2a6e258bfd66186542de71b2cd60790047a2d440
# Parent  aa48b37092dffa6bc2d2e13ff3ee512309f1d10f
fixed (?) LaTeX presentation

diff -r aa48b37092df -r 2a6e258bfd66 src/HOL/Algebra/Embedded_Algebras.thy
--- a/src/HOL/Algebra/Embedded_Algebras.thy	Mon Jul 02 15:43:22 2018 +0100
+++ b/src/HOL/Algebra/Embedded_Algebras.thy	Mon Jul 02 16:20:03 2018 +0100
@@ -122,7 +122,7 @@
 qed
 
 
-subsection \<open>Some Basic Properties of Linear_Ind\<close>
+subsection \<open>Some Basic Properties of Linear Independence\<close>
 
 lemma independent_in_carrier: "independent K Us \<Longrightarrow> set Us \<subseteq> carrier R"
   by (induct Us rule: independent.induct) (simp_all)
@@ -362,7 +362,7 @@
   using Span_eq_combine_set_length_version[OF assms] by blast
 
 
-subsection \<open>Span as the minimal subgroup that contains K <#> (set Us)\<close>
+subsection \<open>Span as the minimal subgroup that contains @{term"K <#> (set Us)"}\<close>
 
 text \<open>Now we show the link between Span and Group.generate\<close>