improved mutabelle script to use nat for quickcheck_narrowing
authorbulwahn
Tue, 14 Jun 2011 08:33:51 +0200
changeset 44251809de915155f
parent 44250 8c4b383e5143
child 44252 9cd4b4ecb4dd
child 44253 806878ae2219
improved mutabelle script to use nat for quickcheck_narrowing
src/HOL/Mutabelle/lib/Tools/mutabelle
     1.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Tue Jun 14 08:30:19 2011 +0200
     1.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Tue Jun 14 08:33:51 2011 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4    MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
     1.5    MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
     1.6    MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
     1.7 -    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ int}])))) \"narrowing_nat\"  
     1.8 +    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"  
     1.9  (*  MutabelleExtra.nitpick_mtd *)
    1.10  ]
    1.11  *}