# HG changeset patch
# User bulwahn
# Date 1280650543 -7200
# Node ID 5ae05823cfd9b2b31d1d010a9681333bdfff0a71
# Parent  823b1e8bc0901fda051321675f7907a5c4e162af
setting up Code_Prolog_Examples

diff -r 823b1e8bc090 -r 5ae05823cfd9 src/HOL/Library/Code_Prolog.thy
--- /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
+
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 *}
diff -r 823b1e8bc090 -r 5ae05823cfd9 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- 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"];