| changeset 30152 | 0ddd8028f98c |
| parent 30151 | 629f3a92863e |
| parent 30148 | 5d04b67a866e |
| child 30153 | 051d3825a15d |
| 30151:629f3a92863e | 30152:0ddd8028f98c |
|---|---|
1 |
|
2 (* $Id$ *) |
|
3 |
|
4 theory "locale" imports base begin |
|
5 |
|
6 chapter {* Structured specifications *} |
|
7 |
|
8 section {* Specification elements *} |
|
9 |
|
10 text FIXME |
|
11 |
|
12 |
|
13 section {* Type-inference *} |
|
14 |
|
15 text FIXME |
|
16 |
|
17 |
|
18 section {* Local theories *} |
|
19 |
|
20 text {* |
|
21 FIXME |
|
22 |
|
23 \glossary{Local theory}{FIXME} |
|
24 *} |
|
25 |
|
26 end |