doc-src/IsarImplementation/Thy/locale.thy
changeset 30101 5c6efec476ae
parent 30100 e1c714d33c5c
parent 29777 f3284860004c
child 30105 37f47ea6fed1
equal deleted inserted replaced
30100:e1c714d33c5c 30101:5c6efec476ae
     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