1.1 --- a/doc-src/IsarRef/syntax.tex	Wed Dec 01 18:17:01 2004 +0100
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Thu Dec 02 00:44:54 2004 +0100
     1.3 @@ -405,16 +405,13 @@
     1.4  
     1.5  \subsection{Antiquotations}\label{sec:antiq}
     1.6  
     1.7 -\begin{matharray}{rcl}
     1.8 -  thm & : & \isarantiq \\
     1.9 -  prop & : & \isarantiq \\
    1.10 -  term & : & \isarantiq \\
    1.11 -  typ & : & \isarantiq \\
    1.12 -  text & : & \isarantiq \\
    1.13 -  goals & : & \isarantiq \\
    1.14 -  subgoals & : & \isarantiq \\
    1.15 -  prf & : & \isarantiq \\
    1.16 -  full_prf & : & \isarantiq \\
    1.17 +\begin{matharray}{rcl@{\hspace*{2cm}}rcl}
    1.18 +  thm & : & \isarantiq & text & : & \isarantiq \\
    1.19 +  lhs & : & \isarantiq & goals & : & \isarantiq \\
    1.20 +  rhs & : & \isarantiq & subgoals & : & \isarantiq \\
    1.21 +  prop & : & \isarantiq & prf & : & \isarantiq \\
    1.22 +  term & : & \isarantiq & full_prf & : & \isarantiq \\
    1.23 +  typ & : & \isarantiq \\  
    1.24  \end{matharray}
    1.25  
    1.26  The text body of formal comments (see also \S\ref{sec:comments}) may contain
    1.27 @@ -432,7 +429,7 @@
    1.28  statement where all schematic variables have been replaced by fixed ones,
    1.29  which are easier to read.
    1.30  
    1.31 -\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
    1.32 +\indexisarant{thm}\indexisarant{lhs}\indexisarant{rhs}\indexisarant{prop}\indexisarant{term}
    1.33  \indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
    1.34  \begin{rail}
    1.35    atsign lbrace antiquotation rbrace
    1.36 @@ -440,6 +437,8 @@
    1.37  
    1.38    antiquotation:
    1.39      'thm' options thmrefs |
    1.40 +    'lhs' options thmrefs |
    1.41 +    'rhs' options thmrefs |
    1.42      'prop' options prop |
    1.43      'term' options term |
    1.44      'typ' options type |
    1.45 @@ -465,6 +464,15 @@
    1.46    $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
    1.47    useful to suppress printing of schematic variables.
    1.48  
    1.49 +\item [$\at\{lhs~\vec a\}$] prints the left hand sides of theorems $\vec a$.
    1.50 +  The antiquotation only works for $\vec a$ that are definitions,
    1.51 +  equations or other binary operators.  It understands the same
    1.52 +  options and attributes as $\at\{thm~\vec a\}$.
    1.53 +
    1.54 +\item [$\at\{rhs~\vec a\}$] prints the right hand sides of theorems $\vec a$.
    1.55 +  As for $\at\{lhs~\vec a\}$, $\vec a$ must be definitions, equations or
    1.56 +  other binary operators.
    1.57 +
    1.58  \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
    1.59  
    1.60  \item [$\at\{term~t\}$] prints a well-typed term $t$.