src/HOL/Library/Code_Prolog.thy
author wenzelm
Thu Feb 16 22:53:24 2012 +0100 (2012-02-16)
changeset 46507 1b24c24017dd
parent 38731 2c8a595af43e
child 47108 2a1953f0d20d
permissions -rw-r--r--
tuned proofs;
bulwahn@38117
     1
(*  Title:      HOL/Library/Code_Prolog.thy
bulwahn@38117
     2
    Author:     Lukas Bulwahn, TUM 2010
bulwahn@38117
     3
*)
bulwahn@38117
     4
bulwahn@38117
     5
header {* Code generation of prolog programs *}
bulwahn@38117
     6
bulwahn@38117
     7
theory Code_Prolog
bulwahn@38117
     8
imports Main
bulwahn@38117
     9
uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
bulwahn@38117
    10
begin
bulwahn@38117
    11
bulwahn@38731
    12
section {* Setup for Numerals *}
bulwahn@38731
    13
bulwahn@38731
    14
setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
bulwahn@38731
    15
setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
bulwahn@38731
    16
bulwahn@38117
    17
end
bulwahn@38117
    18