author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 55447 | aa41ecbdc205 |
child 58881 | b9556a055632 |
permissions | -rw-r--r-- |
38117 | 1 |
(* Title: HOL/Library/Code_Prolog.thy |
2 |
Author: Lukas Bulwahn, TUM 2010 |
|
3 |
*) |
|
4 |
||
5 |
header {* Code generation of prolog programs *} |
|
6 |
||
7 |
theory Code_Prolog |
|
8 |
imports Main |
|
55447 | 9 |
keywords "values_prolog" :: diag |
38117 | 10 |
begin |
11 |
||
48891 | 12 |
ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" |
13 |
||
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38117
diff
changeset
|
14 |
section {* Setup for Numerals *} |
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38117
diff
changeset
|
15 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
48891
diff
changeset
|
16 |
setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *} |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
38731
diff
changeset
|
17 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
48891
diff
changeset
|
18 |
setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *} |
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38117
diff
changeset
|
19 |
|
38117 | 20 |
end |