checked Struct_Deriv.thy ok for analogy in scala decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Thu, 18 Nov 2010 18:25:05 +0100
branchdecompose-isar
changeset 38071679dd9ebb17b
parent 38069 43bf3a5d37b8
child 38072 a6ce90b2f06a
checked Struct_Deriv.thy ok for analogy in scala
test/Pure/Isar/Struct_Deriv.thy
     1.1 --- a/test/Pure/Isar/Struct_Deriv.thy	Thu Nov 18 17:41:20 2010 +0100
     1.2 +++ b/test/Pure/Isar/Struct_Deriv.thy	Thu Nov 18 18:25:05 2010 +0100
     1.3 @@ -17,9 +17,19 @@
     1.4  1.1.3. parser setup according to src/Pure/Isar/outer_syntax.ML
     1.5  1.2. build parser for SD
     1.6  1.2.1. fun parse by Stefan Berghofer
     1.7 -1.2.2. examples
     1.8 -1.2.3. parsers for the "executable" elements
     1.9 -1.2.4. GOON ?  
    1.10 +2. provisional parser for SD
    1.11 +2.1. calc elements to be executed separately
    1.12 +2.1.1. named_rule
    1.13 +2.1.2. term_rule
    1.14 +2.1.3. rule
    1.15 +2.1.4. PBLheadline
    1.16 +2.1.5. CASheadline
    1.17 +2.1.6. headline
    1.18 +2.1.7. calcline
    1.19 +2.2. parser for a whole SD
    1.20 +2.2.1. provisional parser setup
    1.21 +2.2.2. parser applied to example 1
    1.22 +2.2.3. parser applied to example 2
    1.23  *}
    1.24  
    1.25  section {* provisional parser setup *}