| changeset 65552 | f533820e7248 |
| parent 62348 | 9a5f43dac883 |
| child 67399 | eab6ce8368fa |
--- a/src/HOL/ex/LocaleTest2.thy Sat Apr 22 12:52:55 2017 +0200 +++ b/src/HOL/ex/LocaleTest2.thy Sat Apr 22 22:01:35 2017 +0200 @@ -11,7 +11,7 @@ section \<open>Test of Locale Interpretation\<close> theory LocaleTest2 -imports Main GCD +imports Main begin section \<open>Interpretation of Defined Concepts\<close>