1.1 --- a/src/Doc/Codegen/Inductive_Predicate.thy Sun Feb 24 18:30:35 2013 +0100
1.2 +++ b/src/Doc/Codegen/Inductive_Predicate.thy Sun Feb 24 20:18:32 2013 +0100
1.3 @@ -265,7 +265,7 @@
1.4
1.5 text {*
1.6 Further examples for compiling inductive predicates can be found in
1.7 - the @{text "HOL/ex/Predicate_Compile_ex.thy"} theory file. There are
1.8 + the @{text "HOL/Predicate_Compile_Examples.thy"} theory file. There are
1.9 also some examples in the Archive of Formal Proofs, notably in the
1.10 @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
1.11 sessions.