# 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"];