equal
deleted
inserted
replaced
107 results in @{thm conjI[no_vars]}. |
107 results in @{thm conjI[no_vars]}. |
108 |
108 |
109 This \verb!no_vars! business can become a bit tedious. |
109 This \verb!no_vars! business can become a bit tedious. |
110 If you would rather never see question marks, simply put |
110 If you would rather never see question marks, simply put |
111 \begin{verbatim} |
111 \begin{verbatim} |
112 reset show_var_qmarks; |
112 reset show_question_marks; |
113 \end{verbatim} |
113 \end{verbatim} |
114 at the beginning of your file \texttt{ROOT.ML}. |
114 at the beginning of your file \texttt{ROOT.ML}. |
115 The rest of this document is produced with this flag reset. |
115 The rest of this document is produced with this flag reset. |
116 *} |
116 *} |
117 |
117 |
118 (*<*)ML"reset show_var_qmarks"(*>*) |
118 (*<*)ML"reset show_question_marks"(*>*) |
119 |
119 |
120 subsection "Inference rules" |
120 subsection "Inference rules" |
121 |
121 |
122 text{* To print theorems as inference rules you need to include Didier |
122 text{* To print theorems as inference rules you need to include Didier |
123 R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
123 R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
337 \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ |
337 \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ |
338 \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\ |
338 \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\ |
339 \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\ |
339 \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\ |
340 \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ |
340 \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ |
341 \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ |
341 \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ |
342 \verb! in [TermStyle.update_style "new_lhs" my_lhs]!\\ |
342 \verb! in [TermStyle.add_style "new_lhs" my_lhs]!\\ |
343 \verb!end;!\\ |
343 \verb!end;!\\ |
344 \verb!*!\verb!}!\\ |
344 \verb!*!\verb!}!\\ |
345 \end{quote} |
345 \end{quote} |
346 |
346 |
347 This example indeed shows a way the \verb!lhs! style could be implemented; |
347 This example indeed shows a way the \verb!lhs! style could be implemented; |