ProgTutorial/Package/Ind_Interface.thy
changeset 517 d8c376662bb4
parent 514 7e25716c3744
child 535 5734ab5dd86d
equal deleted inserted replaced
516:fb6c29a90003 517:d8c376662bb4
    59   Figure~\ref{fig:specs}. The syntax used in these examples more or
    59   Figure~\ref{fig:specs}. The syntax used in these examples more or
    60   less translates directly into the parser:
    60   less translates directly into the parser:
    61 
    61 
    62 *}
    62 *}
    63 
    63 
    64 ML{*val spec_parser = 
    64 ML %grayML{*val spec_parser = 
    65    Parse.fixes -- 
    65    Parse.fixes -- 
    66    Scan.optional 
    66    Scan.optional 
    67      (Parse.$$$ "where" |--
    67      (Parse.$$$ "where" |--
    68         Parse.!!! 
    68         Parse.!!! 
    69           (Parse.enum1 "|" 
    69           (Parse.enum1 "|"