isabelle: src/HOL/Library/Code_Prolog.thy@c05e8209a3aa (annotated)

38117 5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	1	(* Title: HOL/Library/Code_Prolog.thy
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	2	Author: Lukas Bulwahn, TUM 2010
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	3	*)
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	4
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	5	header {* Code generation of prolog programs *}
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	6
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	7	theory Code_Prolog
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	8	imports Main
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	9	uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	10	begin
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	11
38731 2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	12	section {* Setup for Numerals *}
2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	13
2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	14	setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	15	setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	16
38117 5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	17	end
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	18

author	huffman
	Wed, 23 Nov 2011 07:00:01 +0100
changeset 45615	c05e8209a3aa
parent 38731	2c8a595af43e
child 47108	2a1953f0d20d
permissions	-rw-r--r--