| changeset 23219 | 87ad6e8a5f2c |
| parent 22757 | d3298d63b7b6 |
| child 23919 | af871d13e320 |
--- 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 *}