--- 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 {*
--- 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>
--- 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%
%
--- 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