test/Pure/Isar/Struct_Deriv.thy
branchdecompose-isar
changeset 38071 679dd9ebb17b
parent 38069 43bf3a5d37b8
child 38072 a6ce90b2f06a
equal deleted inserted replaced
38069:43bf3a5d37b8 38071:679dd9ebb17b
    15 1.1.1. keywords according to src/Pure/Isar/keyword.ML
    15 1.1.1. keywords according to src/Pure/Isar/keyword.ML
    16 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML
    16 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML
    17 1.1.3. parser setup according to src/Pure/Isar/outer_syntax.ML
    17 1.1.3. parser setup according to src/Pure/Isar/outer_syntax.ML
    18 1.2. build parser for SD
    18 1.2. build parser for SD
    19 1.2.1. fun parse by Stefan Berghofer
    19 1.2.1. fun parse by Stefan Berghofer
    20 1.2.2. examples
    20 2. provisional parser for SD
    21 1.2.3. parsers for the "executable" elements
    21 2.1. calc elements to be executed separately
    22 1.2.4. GOON ?  
    22 2.1.1. named_rule
       
    23 2.1.2. term_rule
       
    24 2.1.3. rule
       
    25 2.1.4. PBLheadline
       
    26 2.1.5. CASheadline
       
    27 2.1.6. headline
       
    28 2.1.7. calcline
       
    29 2.2. parser for a whole SD
       
    30 2.2.1. provisional parser setup
       
    31 2.2.2. parser applied to example 1
       
    32 2.2.3. parser applied to example 2
    23 *}
    33 *}
    24 
    34 
    25 section {* provisional parser setup *}
    35 section {* provisional parser setup *}
    26 
    36 
    27 subsection {* keywords, outer syntax and parser setup *}
    37 subsection {* keywords, outer syntax and parser setup *}