isabelle: src/HOL/Library/Code_Prolog.thy@c0eafbd55de3 (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	begin
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47108 diff changeset	11	ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47108 diff changeset	12
38731 2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	13	section {* Setup for Numerals *}
2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	14
47108 2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 38731 diff changeset	15	setup {* Predicate_Compile_Data.ignore_consts
2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 38731 diff changeset	16	[@{const_name numeral}, @{const_name neg_numeral}] *}
2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 38731 diff changeset	17
2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 38731 diff changeset	18	setup {* Predicate_Compile_Data.keep_functions
2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 38731 diff changeset	19	[@{const_name numeral}, @{const_name neg_numeral}] *}
38731 2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	20
38117 5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	21	end

author	wenzelm
	Wed, 22 Aug 2012 22:55:41 +0200
changeset 48891	c0eafbd55de3
parent 47108	2a1953f0d20d
child 54489	03ff4d1e6784
permissions	-rw-r--r--