src/HOL/Library/Code_Prolog.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 38731 2c8a595af43e
child 47108 2a1953f0d20d
permissions -rw-r--r--
Quotient_Info stores only relation maps
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