src/HOL/Library/Code_Prolog.thy
author huffman
Sun, 25 Mar 2012 20:15:39 +0200
changeset 47108 2a1953f0d20d
parent 38731 2c8a595af43e
child 48891 c0eafbd55de3
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
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
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
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 38731
diff changeset
    14
setup {* Predicate_Compile_Data.ignore_consts
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 38731
diff changeset
    15
  [@{const_name numeral}, @{const_name neg_numeral}] *}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 38731
diff changeset
    16
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 38731
diff changeset
    17
setup {* Predicate_Compile_Data.keep_functions
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 38731
diff changeset
    18
  [@{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
    19
38117
5ae05823cfd9 setting up Code_Prolog_Examples
bulwahn
parents:
diff changeset
    20
end