setting up Code_Prolog_Examples

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Prolog.thy	Sun Aug 01 10:15:43 2010 +0200
@@ -0,0 +1,13 @@
+(*  Title:      HOL/Library/Code_Prolog.thy
+    Author:     Lukas Bulwahn, TUM 2010
+*)
+
+header {* Code generation of prolog programs *}
+
+theory Code_Prolog
+imports Main
+uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+begin
+
+end
+

--- 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 *}

--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sun Aug 01 10:15:43 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sun Aug 01 10:15:43 2010 +0200
@@ -1,1 +1,2 @@
 use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
+use_thys ["Code_Prolog_Examples"];