--- a/src/Doc/Datatypes/Datatypes.thy Thu Oct 01 18:44:48 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Oct 01 18:59:53 2015 +0200
@@ -77,8 +77,7 @@
infinite branching.
The package is part of @{theory Main}. Additional functionality is provided by
-the theory @{theory BNF_Axiomatization}, located in the directory
-\verb|~~/src/HOL/Library|.
+the theory @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"}.
The package, like its predecessor, fully adheres to the LCF philosophy
@{cite mgordon79}: The characteristic theorems associated with the specified
@@ -162,7 +161,7 @@
text {*
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
-\verb|~~/src/HOL/|\allowbreak\verb|Datatype_Examples|.
+@{file "~~/src/HOL/Datatype_Examples"}
*}
@@ -1185,7 +1184,7 @@
text {*
Primitive recursion is illustrated through concrete examples based on the
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
-examples can be found in the directory \verb|~~/src/HOL/Datatype_Examples|.
+examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
*}
@@ -1258,7 +1257,7 @@
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
\keyw{simps_of_case} command provided by the theory
-\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
+@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
*}
simps_of_case at_simps: at.simps
@@ -1689,9 +1688,9 @@
Codatatypes can be specified using the @{command codatatype} command. The
command is first illustrated through concrete examples featuring different
flavors of corecursion. More examples can be found in the directory
-\verb|~~/src/HOL/|\allowbreak\verb|Datatype_Examples|. The
-\emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
-for lazy lists @{cite "lochbihler-2010"}.
+@{file "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
+includes some useful codatatypes, notably for lazy lists @{cite
+"lochbihler-2010"}.
*}
@@ -1961,8 +1960,8 @@
Corecursive functions can be specified using the @{command primcorec} and
\keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or
using the more general \keyw{partial_function} command. In this tutorial, the
-focus is on the first two. More examples can be found in the directory
-\verb|~~/src/HOL/Datatype_|\allowbreak\verb|Examples|.
+focus is on the first two. More examples can be found in %the directory
+@{file "~~/src/HOL/Datatype_Examples"}.
Whereas recursive functions consume datatypes one constructor at a time,
corecursive functions construct codatatypes one constructor at a time.
@@ -2006,8 +2005,8 @@
text {*
Primitive corecursion is illustrated through concrete examples based on the
codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
-examples can be found in the directory \verb|~~/src/HOL/Datatype_Examples|. The
-code view is favored in the examples below. Sections
+examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
+The code view is favored in the examples below. Sections
\ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
present the same examples expressed using the constructor and destructor views.
*}
@@ -2064,7 +2063,7 @@
\noindent
Pattern matching is not supported by @{command primcorec}. Fortunately, it is
easy to generate pattern-maching equations using the \keyw{simps_of_case}
-command provided by the theory \verb|~~/src/HOL/Library/Simps_Case_Conv|.
+command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
*}
simps_of_case lappend_simps: lappend.code
@@ -2694,8 +2693,7 @@
text {*
The example below shows how to register a type as a BNF using the @{command bnf}
command. Some of the proof obligations are best viewed with the theory
-@{theory Cardinal_Notations}, located in \verb|~~/src/HOL/Library|,
-imported.
+@{file "~~/src/HOL/Library/Cardinal_Notations.thy"} imported.
The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
is live and @{typ 'd} is dead. We introduce it together with its map function,
@@ -2788,10 +2786,10 @@
This particular example does not need any nonemptiness witness, because the
one generated by default is good enough, but in general this would be
-necessary. See \verb|~~/src/HOL/Basic_BNFs.thy|,
-\verb|~~/src/HOL/Library/FSet.thy|, and \verb|~~/src/HOL/Library/Multiset.thy|
-for further examples of BNF registration, some of which feature custom
-witnesses.
+necessary. See @{file "~~/src/HOL/Basic_BNFs.thy"},
+@{file "~~/src/HOL/Library/FSet.thy"}, and
+@{file "~~/src/HOL/Library/Multiset.thy"} for further examples of BNF
+registration, some of which feature custom witnesses.
For many typedefs, lifting the BNF structure from the raw type to the abstract
type can be done uniformly. This is the task of the @{command lift_bnf} command.
@@ -3018,8 +3016,8 @@
The command is useful to reason abstractly about BNFs. The axioms are safe
because there exist BNFs of arbitrary large arities. Applications must import
-the theory @{theory BNF_Axiomatization}, located in the directory
-\verb|~~/src/|\allowbreak\verb|HOL/Library|, to use this functionality.
+the @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"} theory
+to use this functionality.
*}