src/HOL/Library/Nested_Environment.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 18153 a084aa91f701
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     4 *)
     4 *)
     5 
     5 
     6 header {* Nested environments *}
     6 header {* Nested environments *}
     7 
     7 
     8 theory Nested_Environment
     8 theory Nested_Environment
     9 import Main
     9 imports Main
    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