equal
deleted
inserted
replaced
4 Author: Clemens Ballarin, started 31 January 2003 |
4 Author: Clemens Ballarin, started 31 January 2003 |
5 Copyright (c) 2003 by Clemens Ballarin |
5 Copyright (c) 2003 by Clemens Ballarin |
6 *) |
6 *) |
7 |
7 |
8 (*<*) |
8 (*<*) |
9 theory Locales = Main: |
9 theory Locales imports Main begin |
10 |
10 |
11 ML_setup {* print_mode := "type_brackets" :: !print_mode; *} |
11 ML_setup {* print_mode := "type_brackets" :: !print_mode; *} |
12 (*>*) |
12 (*>*) |
13 |
13 |
14 section {* Overview *} |
14 section {* Overview *} |