equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 header {* |
7 header {* Nested environments *} |
8 \title{Nested environments} |
|
9 \author{Markus Wenzel} |
|
10 *} |
|
11 |
8 |
12 theory Nested_Environment = Main: |
9 theory Nested_Environment = Main: |
13 |
10 |
14 text {* |
11 text {* |
15 Consider a partial function @{term [source] "e :: 'a => 'b option"}; |
12 Consider a partial function @{term [source] "e :: 'a => 'b option"}; |