--- 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.