--- a/src/Doc/Codegen/Adaptation.thy Mon Jul 15 19:51:09 2013 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Mon Jul 15 20:13:30 2013 +0200
@@ -119,7 +119,7 @@
The @{theory HOL} @{theory Main} theory already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
- theories in @{text "HOL/Library"}; beside being useful in
+ theories in @{file "~~/src/HOL/Library"}; beside being useful in
applications, they may serve as a tutorial for customising the code
generator setup (see below \secref{sec:adaptation_mechanisms}).
--- a/src/Doc/Codegen/Further.thy Mon Jul 15 19:51:09 2013 +0200
+++ b/src/Doc/Codegen/Further.thy Mon Jul 15 20:13:30 2013 +0200
@@ -222,7 +222,7 @@
subsection {* Parallel computation *}
text {*
- Theory @{text Parallel} in @{text "HOL/Library"} contains
+ Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
operations to exploit parallelism inside the Isabelle/ML
runtime engine.
*}
--- a/src/Doc/Codegen/Inductive_Predicate.thy Mon Jul 15 19:51:09 2013 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Mon Jul 15 20:13:30 2013 +0200
@@ -265,7 +265,7 @@
text {*
Further examples for compiling inductive predicates can be found in
- the @{text "HOL/Predicate_Compile_Examples.thy"} theory file. There are
+ @{file "~~/src/HOL/Predicate_Compile_Examples"}. There are
also some examples in the Archive of Formal Proofs, notably in the
@{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
sessions.