# HG changeset patch
# User nipkow
# Date 1117004633 -7200
# Node ID 0e7b145c3a89c1f5313e61c3e48343bb46ca5378
# Parent  c57725e8055a4f5f570f1e05e48034524d9fd3c8
grammar

diff -r c57725e8055a -r 0e7b145c3a89 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Wed May 25 02:49:46 2005 +0200
+++ b/doc-src/IsarRef/syntax.tex	Wed May 25 09:03:53 2005 +0200
@@ -490,7 +490,7 @@
   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$, previously
+\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\{text~s\}$] prints uninterpreted source text $s$.  This is