diff -r 0460ff79bb52 -r d87d85a5d9ab src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Mar 24 17:40:43 2010 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Mar 24 17:40:44 2010 +0100 @@ -1,5 +1,5 @@ theory Predicate_Compile_Examples -imports "../ex/Predicate_Compile_Alternative_Defs" +imports Predicate_Compile_Alternative_Defs begin subsection {* Basic predicates *}