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 \Volume of a simplex\ +section%important \Volume of a Simplex\ + theory Simplex_Content - imports Change_Of_Vars +imports Change_Of_Vars begin lemma fact_neq_top_ennreal [simp]: "fact n \ (top :: ennreal)"