src/HOL/Library/Code_Prolog.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69605 a96320074298
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Title:      HOL/Library/Code_Prolog.thy
     2     Author:     Lukas Bulwahn, TUM 2010
     3 *)
     4 
     5 section \<open>Code generation of prolog programs\<close>
     6 
     7 theory Code_Prolog
     8 imports Main
     9 keywords "values_prolog" :: diag
    10 begin
    11 
    12 ML_file \<open>~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML\<close>
    13 
    14 section \<open>Setup for Numerals\<close>
    15 
    16 setup \<open>Predicate_Compile_Data.ignore_consts [\<^const_name>\<open>numeral\<close>]\<close>
    17 
    18 setup \<open>Predicate_Compile_Data.keep_functions [\<^const_name>\<open>numeral\<close>]\<close>
    19 
    20 end