equal
deleted
inserted
replaced
2585 \begin{readmore} |
2585 \begin{readmore} |
2586 The general infrastructure for pretty-printing is implemented in the file |
2586 The general infrastructure for pretty-printing is implemented in the file |
2587 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"} |
2587 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"} |
2588 contains pretty-printing functions for terms, types, theorems and so on. |
2588 contains pretty-printing functions for terms, types, theorems and so on. |
2589 |
2589 |
2590 @{ML_file "Pure/General/markup.ML"} |
2590 @{ML_file "Pure/PIDE/markup.ML"} |
2591 \end{readmore} |
2591 \end{readmore} |
2592 *} |
2592 *} |
2593 |
2593 |
2594 section {* Summary *} |
2594 section {* Summary *} |
2595 |
2595 |