# HG changeset patch
# User haftmann
# Date 1329594819 -3600
# Node ID af3df09590f9be49170787b254d72ef044a7fc67
# Parent  8d51b375e926b5cc8981c51ecbea88807773fef0
updated generated documents

diff -r 8d51b375e926 -r af3df09590f9 doc-src/IsarImplementation/Thy/document/Proof.tex
--- 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%
diff -r 8d51b375e926 -r af3df09590f9 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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%
diff -r 8d51b375e926 -r af3df09590f9 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- 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}%
diff -r 8d51b375e926 -r af3df09590f9 doc-src/TutorialI/Types/document/Axioms.tex
--- 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%