# HG changeset patch
# User wenzelm
# Date 1329324543 -3600
# Node ID 50fca9d09528bb138e11240261dba68ab7400c43
# Parent  10a9c31a22b4790502d36177c19b629b633ef198
updated refs;

diff -r 10a9c31a22b4 -r 50fca9d09528 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Feb 15 13:24:22 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Feb 15 17:49:03 2012 +0100
@@ -748,12 +748,12 @@
   collection of Isabelle regular symbols.
 
   \medskip Output of Isabelle symbols depends on the print mode
-  (\secref{print-mode}).  For example, the standard {\LaTeX} setup of
-  the Isabelle document preparation system would present
+  (\cite{isabelle-isar-ref}).  For example, the standard {\LaTeX}
+  setup of the Isabelle document preparation system would present
   ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
-  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
-  "\<^bold>\<alpha>"}.  On-screen rendering usually works by mapping a finite
-  subset of Isabelle symbols to suitable Unicode characters.
+  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text "\<^bold>\<alpha>"}.
+  On-screen rendering usually works by mapping a finite subset of
+  Isabelle symbols to suitable Unicode characters.
 *}
 
 text %mlref {*
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 \<Rightarrow> bool) \<Rightarrow>
diff -r 10a9c31a22b4 -r 50fca9d09528 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Feb 15 13:24:22 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Feb 15 17:49:03 2012 +0100
@@ -1133,11 +1133,12 @@
   collection of Isabelle regular symbols.
 
   \medskip Output of Isabelle symbols depends on the print mode
-  (\secref{print-mode}).  For example, the standard {\LaTeX} setup of
-  the Isabelle document preparation system would present
+  (\cite{isabelle-isar-ref}).  For example, the standard {\LaTeX}
+  setup of the Isabelle document preparation system would present
   ``\verb,\,\verb,<alpha>,'' as \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, and
-  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  On-screen rendering usually works by mapping a finite
-  subset of Isabelle symbols to suitable Unicode characters.%
+  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.
+  On-screen rendering usually works by mapping a finite subset of
+  Isabelle symbols to suitable Unicode characters.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 10a9c31a22b4 -r 50fca9d09528 doc-src/IsarImplementation/Thy/document/Syntax.tex
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex	Wed Feb 15 13:24:22 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex	Wed Feb 15 17:49:03 2012 +0100
@@ -29,7 +29,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 \isa{All\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} such that \isa{All\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}} faithfully represents