# HG changeset patch # User kleing # Date 1101944694 -3600 # Node ID 96698f16e3d948d5f1b8d20e1f91ae2cf40f5abb # Parent cfd08f5e0bdd034f8490524db8019f1ec63edb6b antiquotations lhs and rhs diff -r cfd08f5e0bdd -r 96698f16e3d9 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Wed Dec 01 18:17:01 2004 +0100 +++ b/doc-src/IsarRef/syntax.tex Thu Dec 02 00:44:54 2004 +0100 @@ -405,16 +405,13 @@ \subsection{Antiquotations}\label{sec:antiq} -\begin{matharray}{rcl} - thm & : & \isarantiq \\ - prop & : & \isarantiq \\ - term & : & \isarantiq \\ - typ & : & \isarantiq \\ - text & : & \isarantiq \\ - goals & : & \isarantiq \\ - subgoals & : & \isarantiq \\ - prf & : & \isarantiq \\ - full_prf & : & \isarantiq \\ +\begin{matharray}{rcl@{\hspace*{2cm}}rcl} + thm & : & \isarantiq & text & : & \isarantiq \\ + lhs & : & \isarantiq & goals & : & \isarantiq \\ + rhs & : & \isarantiq & subgoals & : & \isarantiq \\ + prop & : & \isarantiq & prf & : & \isarantiq \\ + term & : & \isarantiq & full_prf & : & \isarantiq \\ + typ & : & \isarantiq \\ \end{matharray} The text body of formal comments (see also \S\ref{sec:comments}) may contain @@ -432,7 +429,7 @@ statement where all schematic variables have been replaced by fixed ones, which are easier to read. -\indexisarant{thm}\indexisarant{prop}\indexisarant{term} +\indexisarant{thm}\indexisarant{lhs}\indexisarant{rhs}\indexisarant{prop}\indexisarant{term} \indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals} \begin{rail} atsign lbrace antiquotation rbrace @@ -440,6 +437,8 @@ antiquotation: 'thm' options thmrefs | + 'lhs' options thmrefs | + 'rhs' options thmrefs | 'prop' options prop | 'term' options term | 'typ' options type | @@ -465,6 +464,15 @@ $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly useful to suppress printing of schematic variables. +\item [$\at\{lhs~\vec a\}$] prints the left hand sides of theorems $\vec a$. + The antiquotation only works for $\vec a$ that are definitions, + equations or other binary operators. It understands the same + options and attributes as $\at\{thm~\vec a\}$. + +\item [$\at\{rhs~\vec a\}$] prints the right hand sides of theorems $\vec a$. + As for $\at\{lhs~\vec a\}$, $\vec a$ must be definitions, equations or + other binary operators. + \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$. \item [$\at\{term~t\}$] prints a well-typed term $t$.