src/HOL/Mutabelle/mutabelle_extra.ML
changeset 46315 40522961d4b1
parent 46314 f6532c597300
child 46326 9a5d8e7684e5
equal deleted inserted replaced
46314:f6532c597300 46315:40522961d4b1
   276  @{const_name Meson.skolem},
   276  @{const_name Meson.skolem},
   277  @{const_name ATP.fequal},
   277  @{const_name ATP.fequal},
   278  @{const_name transfer_morphism},
   278  @{const_name transfer_morphism},
   279  @{const_name enum_prod_inst.enum_all_prod},
   279  @{const_name enum_prod_inst.enum_all_prod},
   280  @{const_name enum_prod_inst.enum_ex_prod},
   280  @{const_name enum_prod_inst.enum_ex_prod},
   281  @{const_name Quickcheck.catch_match}
   281  @{const_name Quickcheck.catch_match},
       
   282  @{const_name Quickcheck_Exhaustive.unknown}
   282  (*@{const_name "==>"}, @{const_name "=="}*)]
   283  (*@{const_name "==>"}, @{const_name "=="}*)]
   283 
   284 
   284 val forbidden_mutant_consts =
   285 val forbidden_mutant_consts =
   285   [
   286   [
   286    (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
   287    (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),