src/HOL/Library/Code_Prolog.thy
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