doc-src/IsarRef/syntax.tex
changeset 15960 9bd6550dc004
parent 15687 8fa8872cdc49
child 16018 3e4e077af2e7
     1.1 --- a/doc-src/IsarRef/syntax.tex	Fri May 13 20:21:41 2005 +0200
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Sat May 14 21:31:13 2005 +0200
     1.3 @@ -412,11 +412,13 @@
     1.4  
     1.5  \begin{matharray}{rcl@{\hspace*{2cm}}rcl}
     1.6    thm & : & \isarantiq & text & : & \isarantiq \\
     1.7 -  lhs & : & \isarantiq & goals & : & \isarantiq \\
     1.8 -  rhs & : & \isarantiq & subgoals & : & \isarantiq \\
     1.9 -  prop & : & \isarantiq & prf & : & \isarantiq \\
    1.10 -  term & : & \isarantiq & full_prf & : & \isarantiq \\
    1.11 +  prop & : & \isarantiq & goals & : & \isarantiq \\
    1.12 +  term & : & \isarantiq & subgoals & : & \isarantiq \\
    1.13 +  const & : & \isarantiq & prf & : & \isarantiq \\
    1.14 +  typeof & : & \isarantiq & full_prf & : & \isarantiq \\
    1.15    typ & : & \isarantiq \\  
    1.16 +  thm_style & : & \isarantiq \\  
    1.17 +  term_style & : & \isarantiq \\  
    1.18  \end{matharray}
    1.19  
    1.20  The text body of formal comments (see also \S\ref{sec:comments}) may contain
    1.21 @@ -442,11 +444,13 @@
    1.22  
    1.23    antiquotation:
    1.24      'thm' options thmrefs |
    1.25 -    'lhs' options thmrefs |
    1.26 -    'rhs' options thmrefs |
    1.27      'prop' options prop |
    1.28      'term' options term |
    1.29 +    'const' options term |
    1.30 +    'typeof' options term |
    1.31      'typ' options type |
    1.32 +    'thm\_style' options style thmref |
    1.33 +    'term\_style' options style term |
    1.34      'text' options name |
    1.35      'goals' options |
    1.36      'subgoals' options |
    1.37 @@ -469,21 +473,23 @@
    1.38    $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
    1.39    useful to suppress printing of schematic variables.
    1.40  
    1.41 -\item [$\at\{lhs~\vec a\}$] prints the left hand sides of theorems $\vec a$.
    1.42 -  The antiquotation only works for $\vec a$ that are definitions,
    1.43 -  equations or other binary operators.  It understands the same
    1.44 -  options and attributes as $\at\{thm~\vec a\}$.
    1.45 -
    1.46 -\item [$\at\{rhs~\vec a\}$] prints the right hand sides of theorems $\vec a$.
    1.47 -  As for $\at\{lhs~\vec a\}$, $\vec a$ must be definitions, equations or
    1.48 -  other binary operators.
    1.49 -
    1.50  \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
    1.51  
    1.52  \item [$\at\{term~t\}$] prints a well-typed term $t$.
    1.53  
    1.54 +\item [$\at\{const~c\}$] prints a well-defined constant $c$.
    1.55 +
    1.56 +\item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.
    1.57 +
    1.58  \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
    1.59  
    1.60 +\item [$\at\{thm_style~s~a\}$] prints theorem $a$, previously
    1.61 +  applying a style $s$ to it; otherwise behaves the same as $\at\{thm~a\}$
    1.62 +  with just one theorem.
    1.63 +
    1.64 +\item [$\at\{term_style~s~t\}$] prints a well-typed term $t$, previously
    1.65 +  applying a style $s$ to it; otherwise behaves the same as $\at\{term~t\}$.
    1.66 +
    1.67  \item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
    1.68    particularly useful to print portions of text according to the Isabelle
    1.69    {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
    1.70 @@ -510,6 +516,24 @@
    1.71  
    1.72  \end{descr}
    1.73  
    1.74 +Per default, each theory contains three default styles for use with
    1.75 +$\at\{thm_style~s~a\}$ and $\at\{term_style~s~t\}$:
    1.76 +
    1.77 +\begin{descr}
    1.78 +
    1.79 +\item [$lhs$] extracts the left hand sides of terms; this style only works
    1.80 +    for terms that are definitions, equations or other binary operators.
    1.81 +
    1.82 +\item [$rhs$] extracts the right hand sides of terms; likewise,
    1.83 +    this style only works
    1.84 +    for terms that are definitions, equations or other binary operators.
    1.85 +
    1.86 +\item [$conlusion$] extracts the conclusion from propositions.
    1.87 +
    1.88 +\end{descr}
    1.89 +
    1.90 +Further styles may be defined at ML level.
    1.91 +
    1.92  \medskip
    1.93  
    1.94  The following options are available to tune the output.  Note that most of