isabelle: src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy@8c20eb9a388d (annotated)

38074 31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	1	theory Code_Prolog_Examples
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	2	imports Predicate_Compile_Alternative_Defs
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	3	uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	4	begin
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	5
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	6	section {* Example append *}
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	7
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	8	inductive append
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	9	where
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	10	"append [] ys ys"
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	11	\| "append xs ys zs ==> append (x # xs) ys (x # zs)"
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	12
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	13	code_pred append .
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	14
38080 8c20eb9a388d cleaning example file; more natural ordering of variable names bulwahn parents: 38075 diff changeset	15	values 3 "{((x::'b list), y, z). append x y z}"
38075 3d5e2b7d1374 adding values command and parsing prolog output bulwahn parents: 38074 diff changeset	16
38074 31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	17	end

author	bulwahn
	Thu, 29 Jul 2010 17:27:58 +0200
changeset 38080	8c20eb9a388d
parent 38075	3d5e2b7d1374
child 38116	823b1e8bc090
permissions	-rw-r--r--