diff -r 823b1e8bc090 -r 5ae05823cfd9 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Sun Aug 01 10:15:43 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Sun Aug 01 10:15:43 2010 +0200 @@ -1,6 +1,5 @@ theory Code_Prolog_Examples -imports Predicate_Compile_Alternative_Defs -uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" +imports Code_Prolog begin section {* Example append *}