doc-src/IsarImplementation/Thy/locale.thy
changeset 30105 37f47ea6fed1
parent 30104 b094999e1d33
parent 30101 5c6efec476ae
child 30106 351fc2f8493d
equal deleted inserted replaced
30104:b094999e1d33 30105:37f47ea6fed1
     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