src/HOL/Tools/SMT/smt_builtin.ML
changeset 41073 07b454783ed8
parent 41072 9f9bc1bdacef
child 41124 1de17a2de5ad
equal deleted inserted replaced
41072:9f9bc1bdacef 41073:07b454783ed8
   224   @{const_name div_class.mod},
   224   @{const_name div_class.mod},
   225   @{const_name inverse_class.divide} ]
   225   @{const_name inverse_class.divide} ]
   226 
   226 
   227 fun is_builtin_ext ctxt (c as (n, _)) ts =
   227 fun is_builtin_ext ctxt (c as (n, _)) ts =
   228   if member (op =) only_partially_supported n then false
   228   if member (op =) only_partially_supported n then false
   229   else is_builtin_fun_ext ctxt c ts
   229   else
       
   230     is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse 
       
   231     is_builtin_fun_ext ctxt c ts
   230 
   232 
   231 end
   233 end