# HG changeset patch # User wenzelm # Date 1116773466 -7200 # Node ID 3e4e077af2e783dd9e4b3915eaf1cd0c9a69d2ae # Parent cb983795bcdf77e50ade6afc6e301d9d3d64f645 tuned antiquotations; diff -r cb983795bcdf -r 3e4e077af2e7 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Sun May 22 16:51:05 2005 +0200 +++ b/doc-src/IsarRef/syntax.tex Sun May 22 16:51:06 2005 +0200 @@ -436,8 +436,11 @@ statement where all schematic variables have been replaced by fixed ones, which are easier to read. -\indexisarant{thm}\indexisarant{lhs}\indexisarant{rhs}\indexisarant{prop}\indexisarant{term} -\indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals} +\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const} +\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style} +\indexisarant{term-style}\indexisarant{text}\indexisarant{goals} +\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf} + \begin{rail} atsign lbrace antiquotation rbrace ; @@ -516,19 +519,19 @@ \end{descr} -Per default, each theory contains three default styles for use with -$\at\{thm_style~s~a\}$ and $\at\{term_style~s~t\}$: +There are a few standard styles for use with $\at\{thm_style~s~a\}$ and +$\at\{term_style~s~t\}$: \begin{descr} - -\item [$lhs$] extracts the left hand sides of terms; this style only works - for terms that are definitions, equations or other binary operators. - -\item [$rhs$] extracts the right hand sides of terms; likewise, - this style only works - for terms that are definitions, equations or other binary operators. - -\item [$conlusion$] extracts the conclusion from propositions. + +\item [$lhs$] extracts the first argument of any application form with at + least two arguments -- typically is meta-level or object-level equality or + any other binary relation. + +\item [$rhs$] similar to $lhs$, but extracts the second argument. + +\item [$conlusion$] extracts the conclusion $C$ from nested meta-level + implications $A@1 \Imp \cdots A@n \Imp C$. \end{descr}