1.1 --- a/src/HOL/IsaMakefile	Thu Jul 29 17:27:52 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 29 17:27:54 2010 +0200
     1.3 @@ -1320,7 +1320,8 @@
     1.4  $(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL			\
     1.5    Predicate_Compile_Examples/ROOT.ML					\
     1.6    Predicate_Compile_Examples/Predicate_Compile_Examples.thy		\
     1.7 -  Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
     1.8 +  Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
     1.9 +  Predicate_Compile_Examples/Code_Prolog_Examples.thy
    1.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
    1.11  
    1.12  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:54 2010 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +theory Code_Prolog_Examples
     2.5 +imports Predicate_Compile_Alternative_Defs
     2.6 +uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
     2.7 +begin
     2.8 +
     2.9 +section {* Example append *}
    2.10 +
    2.11 +inductive append
    2.12 +where
    2.13 +  "append [] ys ys"
    2.14 +| "append xs ys zs ==> append (x # xs) ys (x # zs)"
    2.15 +
    2.16 +code_pred append .
    2.17 +
    2.18 +ML {*
    2.19 +  tracing (Code_Prolog.write_program (Code_Prolog.generate @{context} [@{const_name append}]))
    2.20 +*}
    2.21 +
    2.22 +ML {*
    2.23 +  Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"]
    2.24 +*}
    2.25 +
    2.26 +end