CookBook/Package/Ind_Code.thy
changeset 110 12533bb49615
parent 91 667a0943c40b
child 118 5f003fdf2653
equal deleted inserted replaced
109:b4234e8a0202 110:12533bb49615
    12 
    12 
    13   @{ML_chunk [display,gray] intro_rules}
    13   @{ML_chunk [display,gray] intro_rules}
    14 
    14 
    15 *}
    15 *}
    16 
    16 
    17 text {*
       
    18 
       
    19   @{ML_chunk [display,gray] storing}
       
    20 
       
    21 *}
       
    22 end
    17 end