equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Nested environments *} |
6 header {* Nested environments *} |
7 |
7 |
8 theory Nested_Environment |
8 theory Nested_Environment |
9 imports Plain List |
9 imports Plain "~~/src/HOL/List" |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 Consider a partial function @{term [source] "e :: 'a => 'b option"}; |
13 Consider a partial function @{term [source] "e :: 'a => 'b option"}; |
14 this may be understood as an \emph{environment} mapping indexes |
14 this may be understood as an \emph{environment} mapping indexes |