isabelle: src/HOL/Library/Code_Prolog.thy@6f0e85e16d84 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	5	section \<open>Code generation of prolog programs\<close>
38117 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
55447 aa41ecbdc205 do not redefine outer syntax commands; wenzelm parents: 54489 diff changeset	9	keywords "values_prolog" :: diag
38117 5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	10	begin
5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	11
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 69593 diff changeset	12	ML_file \<open>~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47108 diff changeset	13
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	14	section \<open>Setup for Numerals\<close>
38731 2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	15
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 60500 diff changeset	16	setup \<open>Predicate_Compile_Data.ignore_consts [\<^const_name>\<open>numeral\<close>]\<close>
47108 2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 38731 diff changeset	17
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 60500 diff changeset	18	setup \<open>Predicate_Compile_Data.keep_functions [\<^const_name>\<open>numeral\<close>]\<close>
38731 2c8a595af43e invocation of values for prolog execution does not require invocation of code_pred anymore bulwahn parents: 38117 diff changeset	19
38117 5ae05823cfd9 setting up Code_Prolog_Examples bulwahn parents: diff changeset	20	end

author	paulson
	Fri, 25 Sep 2020 17:13:12 +0100
changeset 72305	6f0e85e16d84
parent 69605	a96320074298
permissions	-rw-r--r--