src/HOL/Library/Code_Prolog.thy
author wenzelm
Fri, 04 Jan 2019 23:22:53 +0100
changeset 69593 3dda49e08b9d
parent 60500 903bb1495239
child 69605 a96320074298
permissions -rw-r--r--
isabelle update -u control_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
    12
ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
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