
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Simplex_Content.thy
--- a/src/HOL/Analysis/Simplex_Content.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Simplex_Content.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -5,9 +5,10 @@
    The content of an n-dimensional simplex, including the formula for the content of a
    triangle and Heron's formula.
 *)
-section%important \<open>Volume of a simplex\<close>
+section%important \<open>Volume of a Simplex\<close>
+
 theory Simplex_Content
-  imports Change_Of_Vars
+imports Change_Of_Vars
 begin
 
 lemma fact_neq_top_ennreal [simp]: "fact n \<noteq> (top :: ennreal)"




