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