# 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