| author | blanchet |
| Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) | |
| changeset 58425 | 246985c6b20b |
| parent 55447 | aa41ecbdc205 |
| child 58881 | b9556a055632 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/Library/Code_Prolog.thy
2 Author: Lukas Bulwahn, TUM 2010
3 *)
5 header {* Code generation of prolog programs *}
7 theory Code_Prolog
8 imports Main
9 keywords "values_prolog" :: diag
10 begin
12 ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
14 section {* Setup for Numerals *}
16 setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
18 setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
20 end