equal
deleted
inserted
replaced
1883 \begin{isabelle} |
1883 \begin{isabelle} |
1884 @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ |
1884 @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ |
1885 @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} |
1885 @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} |
1886 \end{isabelle} |
1886 \end{isabelle} |
1887 |
1887 |
1888 Such theorem styles allow one to print out theorems in documents formatted to |
1888 Such styles allow one to print out theorems in documents formatted to |
1889 ones heart content. Next we explain theorem attributes, which is another |
1889 ones heart content. The styles can also be used in the document |
|
1890 antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"} |
|
1891 and @{text "@{typeof ...}"}. |
|
1892 |
|
1893 Next we explain theorem attributes, which is another |
1890 mechanism for dealing with theorems. |
1894 mechanism for dealing with theorems. |
1891 |
1895 |
1892 \begin{readmore} |
1896 \begin{readmore} |
1893 Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}. |
1897 Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}. |
1894 \end{readmore} |
1898 \end{readmore} |