| changeset 38117 | 5ae05823cfd9 |
| parent 38116 | 823b1e8bc090 |
| child 38727 | c7f5f0b7dc7f |
--- 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 *}