diff -r 56e56a00511e -r 8fe678fd7fe4 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sun Jun 05 11:31:18 2005 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sun Jun 05 11:31:19 2005 +0200
@@ -485,13 +485,12 @@
 \item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.
 
 \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
-
-\item [$\at\{thm_style~s~a\}$] prints theorem $a$, previously
-  applying a style $s$ to it; otherwise behaves the same as $\at\{thm~a\}$
-  with just one theorem.
-
-\item [$\at\{term_style~s~t\}$] prints a well-typed term $t$ after
-  applying a style $s$ to it; otherwise behaves the same as $\at\{term~t\}$.
+  
+\item [$\at\{thm_style~s~a\}$] prints theorem $a$, previously applying a style
+  $s$ to it (see below).
+  
+\item [$\at\{term_style~s~t\}$] prints a well-typed term $t$ after applying a
+  style $s$ to it (see below).
 
 \item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
   particularly useful to print portions of text according to the Isabelle
@@ -503,40 +502,43 @@
   of goal states does not conform to actual human-readable proof documents.
   Please do not include goal states into document output unless you really
   know what you are doing!
-
-\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
-  print the main goal.
-
+  
+\item [$\at\{subgoals\}$] is similar to $goals$, but does not print the main
+  goal.
+  
 \item [$\at\{prf~\vec a\}$] prints the (compact) proof terms corresponding to
-  the theorems $\vec a$. Note that this
-  requires proof terms to be switched on for the current object logic
-  (see the ``Proof terms'' section of the Isabelle reference manual
-  for information on how to do this).
-
-\item [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays
-  the full proof terms, i.e.\ also displays information omitted in
-  the compact proof term, which is denoted by ``$_$'' placeholders there.
+  the theorems $\vec a$. Note that this requires proof terms to be switched on
+  for the current object logic (see the ``Proof terms'' section of the
+  Isabelle reference manual for information on how to do this).
+  
+\item [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays the
+  full proof terms, i.e.\ also displays information omitted in the compact
+  proof term, which is denoted by ``$_$'' placeholders there.
 
 \end{descr}
 
-There are a few standard styles for use with $\at\{thm_style~s~a\}$ and
-$\at\{term_style~s~t\}$:
+\medskip
+
+The following standard styles for use with $thm_style$ and $term_style$ are
+available:
 
 \begin{descr}
   
 \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.
+  least two arguments -- typically meta-level or object-level equality, or any
+  other binary relation.
+  
+\item [$rhs$] is like $lhs$, but extracts the second argument.
   
-\item [$rhs$] similar to $lhs$, but extracts the second argument.
+\item [$concl$] extracts the conclusion $C$ from a nested meta-level
+  implication $A@1 \Imp \cdots A@n \Imp C$.
   
-\item [$conlusion$] extracts the conclusion $C$ from nested meta-level
-  implications $A@1 \Imp \cdots A@n \Imp C$.
+\item [$prem1$, \dots, $prem9$] extract premise number $1$, \dots, $9$,
+  respectively, from a nested meta-level implication $A@1 \Imp \cdots A@n \Imp
+  C$.
 
 \end{descr}
 
-Further styles may be defined at ML level.
-
 \medskip
 
 The following options are available to tune the output.  Note that most of