# HG changeset patch
# User bulwahn
# Date 1307001100 -7200
# Node ID 092e38108f3fcbce891fbd5fbc1c4895e9d72883
# Parent  70337ff0352d59fe5571e7dfeb45d73627ef3157
adding invocation of exhaustive testing without using finite types to mutabelle

diff -r 70337ff0352d -r 092e38108f3f src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Jun 02 09:51:40 2011 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Jun 02 09:51:40 2011 +0200
@@ -87,6 +87,7 @@
 val mtds = [
   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
   MutabelleExtra.nitpick_mtd
 ]
 *}
@@ -124,6 +125,8 @@
 T: $(count "quickcheck_random" "Timeout") E: $(count "quickcheck_random" "Error")"
 echo "exhaustive  : C: $(count "quickcheck_exhaustive" "GenuineCex") N: $(count "quickcheck_exhaustive" "NoCex") \
 T: $(count "quickcheck_exhaustive" "Timeout") E: $(count "quickcheck_exhaustive" "Error")"
+echo "exhaustive_nft: C: $(count "quickcheck_exhaustive_nft" "GenuineCex") N: $(count "quickcheck_exhaustive_nft" "NoCex") \
+T: $(count "quickcheck_exhaustive_nft" "Timeout") E: $(count "quickcheck_exhaustive_nft" "Error")"
 echo "nitpick     : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \
 T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")"