src/HOL/Library/Code_Prolog.thy
author Andreas Lochbihler
Fri Sep 20 10:09:16 2013 +0200 (2013-09-20)
changeset 53745 788730ab7da4
parent 48891 c0eafbd55de3
child 54489 03ff4d1e6784
permissions -rw-r--r--
prefer Code.abort over code_abort
     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
     9 begin
    10 
    11 ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
    12 
    13 section {* Setup for Numerals *}
    14 
    15 setup {* Predicate_Compile_Data.ignore_consts
    16   [@{const_name numeral}, @{const_name neg_numeral}] *}
    17 
    18 setup {* Predicate_Compile_Data.keep_functions
    19   [@{const_name numeral}, @{const_name neg_numeral}] *}
    20 
    21 end