equal
deleted
inserted
replaced
1711 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar |
1711 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar |
1712 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar |
1712 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar |
1713 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} |
1713 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} |
1714 |
1714 |
1715 Here the layout of @{ML test_str} is much more pleasing to the |
1715 Here the layout of @{ML test_str} is much more pleasing to the |
1716 eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no indentation |
1716 eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no hanging |
1717 of the printed string. You can increase the indentation and obtain |
1717 indentation of the printed string. You can increase the indentation |
|
1718 and obtain |
1718 |
1719 |
1719 @{ML_response_fake [display,gray] |
1720 @{ML_response_fake [display,gray] |
1720 "let |
1721 "let |
1721 val ptrs = map Pretty.str (space_explode \" \" test_str) |
1722 val ptrs = map Pretty.str (space_explode \" \" test_str) |
1722 in |
1723 in |
1956 |
1957 |
1957 |
1958 |
1958 |
1959 |
1959 section {* Managing Name Spaces (TBD) *} |
1960 section {* Managing Name Spaces (TBD) *} |
1960 |
1961 |
|
1962 ML {* Sign.intern_type @{theory} "list" *} |
|
1963 ML {* Sign.intern_const @{theory} "prod_fun" *} |
|
1964 |
1961 section {* Summary *} |
1965 section {* Summary *} |
1962 |
1966 |
1963 text {* |
1967 text {* |
1964 \begin{conventions} |
1968 \begin{conventions} |
1965 \begin{itemize} |
1969 \begin{itemize} |