366 (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}). |
366 (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}). |
367 |
367 |
368 Likewise, \verb!concl! may be used as a style to show just the |
368 Likewise, \verb!concl! may be used as a style to show just the |
369 conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
369 conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
370 \begin{center} |
370 \begin{center} |
371 @{thm hd_Cons_tl} |
371 @{thm [show_types] hd_Cons_tl} |
372 \end{center} |
372 \end{center} |
373 To print just the conclusion, |
373 To print just the conclusion, |
374 \begin{center} |
374 \begin{center} |
375 @{thm_style concl hd_Cons_tl} |
375 @{thm_style [show_types] concl hd_Cons_tl} |
376 \end{center} |
376 \end{center} |
377 type |
377 type |
378 \begin{quote} |
378 \begin{quote} |
379 \verb!\begin{center}!\\ |
379 \verb!\begin{center}!\\ |
380 \verb!@!\verb!{thm_style concl hd_Cons_tl}!\\ |
380 \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\ |
381 \verb!\end{center}! |
381 \verb!\end{center}! |
382 \end{quote} |
382 \end{quote} |
|
383 |
|
384 Be aware that any options must be placed \emph{before} |
|
385 the name of the style, as in this example. |
383 |
386 |
384 Further use cases can be found in \S\ref{sec:yourself}. |
387 Further use cases can be found in \S\ref{sec:yourself}. |
385 |
388 |
386 If you are not afraid of ML, you may also define your own styles. |
389 If you are not afraid of ML, you may also define your own styles. |
387 A style is implemented by an ML function of type |
390 A style is implemented by an ML function of type |