src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 37591 d3daea901123
parent 36253 6e969ce3dfcc
child 39198 f967a16dfcdd
equal deleted inserted replaced
37590:180e80b4eac1 37591:d3daea901123
    16 
    16 
    17 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    17 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    18 
    18 
    19 section {* Pairs *}
    19 section {* Pairs *}
    20 
    20 
    21 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
    21 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
    22 
    22 
    23 section {* Bounded quantifiers *}
    23 section {* Bounded quantifiers *}
    24 
    24 
    25 declare Ball_def[code_pred_inline]
    25 declare Ball_def[code_pred_inline]
    26 declare Bex_def[code_pred_inline]
    26 declare Bex_def[code_pred_inline]