adding example file for prolog code generation; adding prolog code generation example to IsaMakefile

--- a/src/HOL/IsaMakefile	Thu Jul 29 17:27:52 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 29 17:27:54 2010 +0200
@@ -1320,7 +1320,8 @@
 $(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL			\
   Predicate_Compile_Examples/ROOT.ML					\
   Predicate_Compile_Examples/Predicate_Compile_Examples.thy		\
-  Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
+  Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
+  Predicate_Compile_Examples/Code_Prolog_Examples.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:54 2010 +0200
@@ -0,0 +1,23 @@
+theory Code_Prolog_Examples
+imports Predicate_Compile_Alternative_Defs
+uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+begin
+
+section {* Example append *}
+
+inductive append
+where
+  "append [] ys ys"
+| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+
+code_pred append .
+
+ML {*
+  tracing (Code_Prolog.write_program (Code_Prolog.generate @{context} [@{const_name append}]))
+*}
+
+ML {*
+  Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"]
+*}
+
+end