equal
deleted
inserted
replaced
20 |
20 |
21 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *} |
21 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *} |
22 |
22 |
23 section {* Pairs *} |
23 section {* Pairs *} |
24 |
24 |
25 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *} |
25 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *} |
26 |
26 |
27 section {* Bounded quantifiers *} |
27 section {* Bounded quantifiers *} |
28 |
28 |
29 declare Ball_def[code_pred_inline] |
29 declare Ball_def[code_pred_inline] |
30 declare Bex_def[code_pred_inline] |
30 declare Bex_def[code_pred_inline] |