equal
deleted
inserted
replaced
387 *} |
387 *} |
388 (*<*) |
388 (*<*) |
389 setup {* |
389 setup {* |
390 let |
390 let |
391 fun my_concl ctxt = Logic.strip_imp_concl |
391 fun my_concl ctxt = Logic.strip_imp_concl |
392 in [TermStyle.add_style "my_concl" my_concl] |
392 in TermStyle.add_style "my_concl" my_concl |
393 end; |
393 end; |
394 *} |
394 *} |
395 (*>*) |
395 (*>*) |
396 text {* |
396 text {* |
397 |
397 |
398 \begin{quote} |
398 \begin{quote} |
399 \verb!setup {!\verb!*!\\ |
399 \verb!setup {!\verb!*!\\ |
400 \verb!let!\\ |
400 \verb!let!\\ |
401 \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\ |
401 \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\ |
402 \verb! in [TermStyle.add_style "my_concl" my_concl]!\\ |
402 \verb! in TermStyle.add_style "my_concl" my_concl!\\ |
403 \verb!end;!\\ |
403 \verb!end;!\\ |
404 \verb!*!\verb!}!\\ |
404 \verb!*!\verb!}!\\ |
405 \end{quote} |
405 \end{quote} |
406 |
406 |
407 \noindent |
407 \noindent |