changeset 38731 | 2c8a595af43e |
parent 38117 | 5ae05823cfd9 |
child 47108 | 2a1953f0d20d |
--- a/src/HOL/Library/Code_Prolog.thy Wed Aug 25 16:59:49 2010 +0200 +++ b/src/HOL/Library/Code_Prolog.thy Wed Aug 25 16:59:50 2010 +0200 @@ -9,5 +9,10 @@ uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" begin +section {* Setup for Numerals *} + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *} +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *} + end