equal
deleted
inserted
replaced
6 Definitions are less natural in FOL, since there is no selection operator. |
6 Definitions are less natural in FOL, since there is no selection operator. |
7 Hence we do them here in HOL, not in the main test suite for locales, |
7 Hence we do them here in HOL, not in the main test suite for locales, |
8 which is FOL/ex/LocaleTest.thy |
8 which is FOL/ex/LocaleTest.thy |
9 *) |
9 *) |
10 |
10 |
11 header {* Test of Locale Interpretation *} |
11 section {* Test of Locale Interpretation *} |
12 |
12 |
13 theory LocaleTest2 |
13 theory LocaleTest2 |
14 imports Main GCD |
14 imports Main GCD |
15 begin |
15 begin |
16 |
16 |