| author | Christian Sternagel |
| Thu Dec 13 13:11:38 2012 +0100 (2012-12-13) | |
| changeset 50516 | ed6b40d15d1c |
| parent 48891 | c0eafbd55de3 |
| child 54489 | 03ff4d1e6784 |
| 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 begin
11 ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
13 section {* Setup for Numerals *}
15 setup {* Predicate_Compile_Data.ignore_consts
16 [@{const_name numeral}, @{const_name neg_numeral}] *}
18 setup {* Predicate_Compile_Data.keep_functions
19 [@{const_name numeral}, @{const_name neg_numeral}] *}
21 end