src/HOL/Mutabelle/lib/Tools/mutabelle

   echo "  Options are:"
   echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
   echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
   echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
   echo "    -N NUMBER    number of lemmas to choose randomly, if not given all lemmas are chosen"
+  echo "    -M NUMBER    number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)"
   echo
   echo "  THEORY is the name of the theory of which all theorems should be"
   echo "  mutated and tested."
   echo
   exit 1

 
 # options
 
 MUTABELLE_IMPORTS=""
 
-while getopts "L:T:O:N:" OPT
+while getopts "L:T:O:N:M:" OPT
 do
   case "$OPT" in
     L)
       MUTABELLE_LOGIC="$OPTARG"
       ;;

     O)      
       MUTABELLE_OUTPUT_PATH="$OPTARG"
       ;;
     N)
       NUMBER_OF_LEMMAS="$OPTARG"
+      ;;
+    M)
+      MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG"
       ;;
     \?)
       usage
       ;;
   esac

 declare [[quickcheck_timeout = 30]]
 
 ML {*
 val mtds = [
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\",
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
-  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\",
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
-  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\",
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
     #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
-
 (*, MutabelleExtra.refute_mtd, *)
   , MutabelleExtra.nitpick_mtd
 
 ]
 *}

 ML {*
 fun mutation_testing_of thy =
   (MutabelleExtra.random_seed := 1.0;
   MutabelleExtra.thms_of false thy $MUTABELLE_FILTER 
   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
-         @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
+         @{theory} $MUTABELLE_NUMBER_OF_MUTANTS mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
 *}
 
 ML {*
   mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
 *}