# HG changeset patch
# User wenzelm
# Date 1373912010 -7200
# Node ID 5f817bad850a6ab6174b61977490283a59c98e88
# Parent  e99a0a43720b1f0303fb1bb4cb63b1c2ddc260ac
prefer @{file} references that are actually checked;

diff -r e99a0a43720b -r 5f817bad850a src/Doc/Codegen/Adaptation.thy
--- 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}).
 
diff -r e99a0a43720b -r 5f817bad850a src/Doc/Codegen/Further.thy
--- 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.
 *}
diff -r e99a0a43720b -r 5f817bad850a src/Doc/Codegen/Inductive_Predicate.thy
--- 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.