src/HOL/Library/Code_Prolog.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 38731 2c8a595af43e
child 47108 2a1953f0d20d
permissions -rw-r--r--
add nat => enat coercion
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