# HG changeset patch
# User bulwahn
# Date 1280417274 -7200
# Node ID 31174744b9a22758fcef6b35ff2955ffd73383ee
# Parent  64062d56ad3cfbbf9d8d15ca8c1109db2a4ae7ce
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile

diff -r 64062d56ad3c -r 31174744b9a2 src/HOL/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
 
 
diff -r 64062d56ad3c -r 31174744b9a2 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- /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