# HG changeset patch
# User wenzelm
# Date 1375037475 -7200
# Node ID 1165f78c16d8f07a4a7995155ea9d6ef2ddc75a2
# Parent  587a4610da9ef693daf5db3dc4c8c5a38ca86316
prefer examples that work out of the box;

diff -r 587a4610da9e -r 1165f78c16d8 src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jul 28 20:50:44 2013 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jul 28 20:51:15 2013 +0200
@@ -265,7 +265,7 @@
 
 text {*
   Further examples for compiling inductive predicates can be found in
-  @{file "~~/src/HOL/Predicate_Compile_Examples"}.  There are
+  @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   sessions.