diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed May 06 23:28:09 2015 +0200 @@ -110,7 +110,7 @@ @{command "print_state"}~@{text "(latex xsymbols)"} prints the current proof state with mathematical symbols and special characters represented in {\LaTeX} source, according to the Isabelle style - @{cite "isabelle-sys"}. + @{cite "isabelle-system"}. Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic way to include formal items into the printed text