diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/LocaleTest2.thy --- a/src/HOL/ex/LocaleTest2.thy Sun Jun 03 23:16:46 2007 +0200 +++ b/src/HOL/ex/LocaleTest2.thy Sun Jun 03 23:16:47 2007 +0200 @@ -19,7 +19,8 @@ ML {* set show_hyps *} ML {* set show_sorts *} -section {* Interpretation of Defined Concepts *} + +subsection {* Interpretation of Defined Concepts *} text {* Naming convention for global objects: prefixes D and d *}