src/HOL/Mutabelle/lib/Tools/mutabelle
changeset 46452 e4f1cda51df6
parent 46310 8af202923906
child 46453 9e83b7c24b05
equal deleted inserted replaced
46451:4989249a4b81 46452:e4f1cda51df6
    99   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\",
    99   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\",
   100   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
   100   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
   101   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
   101   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
   102   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
   102   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
   103     #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
   103     #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
   104 (*
   104 
   105 , MutabelleExtra.refute_mtd,
   105 (*, MutabelleExtra.refute_mtd, *)
   106   MutabelleExtra.nitpick_mtd
   106   , MutabelleExtra.nitpick_mtd
   107 *)
   107 
   108 ]
   108 ]
   109 *}
   109 *}
   110 
   110 
   111 ML {*
   111 ML {*
   112 fun mutation_testing_of thy =
   112 fun mutation_testing_of thy =