diff -r 10a9c31a22b4 -r 50fca9d09528 doc-src/IsarImplementation/Thy/Syntax.thy --- a/doc-src/IsarImplementation/Thy/Syntax.thy Wed Feb 15 13:24:22 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Syntax.thy Wed Feb 15 17:49:03 2012 +0100 @@ -10,7 +10,7 @@ additional means for reading and printing of terms and types. This important add-on outside the logical core is called \emph{inner syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of - the theory and proof language (cf.\ \chref{FIXME}). + the theory and proof language (cf.\ \cite{isabelle-isar-ref}). For example, according to \cite{church40} quantifiers are represented as higher-order constants @{text "All :: ('a \ bool) \