doc-src/IsarRef/syntax.tex
 changeset 16018 3e4e077af2e7 parent 15960 9bd6550dc004 child 16068 0e7b145c3a89
--- 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,

-\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}