equal
deleted
inserted
replaced
50 |
50 |
51 section \<open>Setup for Numerals\<close> |
51 section \<open>Setup for Numerals\<close> |
52 |
52 |
53 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close> |
53 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close> |
54 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close> |
54 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close> |
|
55 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close> |
|
56 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close> |
55 |
57 |
56 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\<close> |
58 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\<close> |
57 |
59 |
58 section \<open>Arithmetic operations\<close> |
60 section \<open>Arithmetic operations\<close> |
59 |
61 |