equal
deleted
inserted
replaced
689 \begin{readmore} |
689 \begin{readmore} |
690 The functions to do with input and output of XML and YXML are defined |
690 The functions to do with input and output of XML and YXML are defined |
691 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}. |
691 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}. |
692 \end{readmore} |
692 \end{readmore} |
693 |
693 |
|
694 FIXME: |
|
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} |
|
697 |
|
698 |
694 *} |
699 *} |
695 |
700 |
696 section {* Parsing Specifications\label{sec:parsingspecs} *} |
701 section {* Parsing Specifications\label{sec:parsingspecs} *} |
697 |
702 |
698 text {* |
703 text {* |