--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Feb 18 20:53:39 2012 +0100
@@ -485,7 +485,7 @@
\begin{isamarkuptext}%
The following example demonstrates how rules can be
derived by building up a context of assumptions first, and exporting
- some local fact afterwards. We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality
+ some local fact afterwards. We refer to \isa{Pure} equality
here for testing purposes.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Feb 18 20:53:39 2012 +0100
@@ -1115,7 +1115,7 @@
%
\begin{isamarkuptext}%
We define a type of finite sequences, with slightly different
- names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \hyperlink{theory.Main}{\mbox{\isa{Main}}}:%
+ names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \isa{Main}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 18 20:53:39 2012 +0100
@@ -1363,12 +1363,12 @@
\item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}.
For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as
- defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
+ defined in theory \isa{List} in Isabelle/HOL.
\item Change of binding status of variables: anything beyond the
built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit
syntax translations. For example, consider list filter
- comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
+ comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \isa{List} in Isabelle/HOL.
\end{itemize}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Axioms.tex Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Sat Feb 18 20:53:39 2012 +0100
@@ -463,7 +463,7 @@
\emph{with} axioms.
Further note that classes may contain axioms but \emph{no} operations.
-An example is class \isa{finite} from theory \hyperlink{theory.Finite-Set}{\mbox{\isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set}}}
+An example is class \isa{finite} from theory \isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set}
which specifies a type to be finite: \isa{{\isaliteral{22}{\isachardoublequote}}finite\ {\isaliteral{28}{\isacharparenleft}}UNIV\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}finite\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.%
\end{isamarkuptext}%
\isamarkuptrue%