equal
deleted
inserted
replaced
692 \end{readmore} |
692 \end{readmore} |
693 |
693 |
694 FIXME: |
694 FIXME: |
695 @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax} |
695 @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax} |
696 @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax} |
696 @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax} |
697 |
697 @{ML_ind read_term in Syntax} @{ML_ind read_term in Syntax} |
|
698 |
698 |
699 |
699 *} |
700 *} |
700 |
701 |
701 section {* Parsing Specifications\label{sec:parsingspecs} *} |
702 section {* Parsing Specifications\label{sec:parsingspecs} *} |
702 |
703 |