equal
deleted
inserted
replaced
81 uses |
81 uses |
82 \"$MUTABELLE_HOME/mutabelle.ML\" |
82 \"$MUTABELLE_HOME/mutabelle.ML\" |
83 \"$MUTABELLE_HOME/mutabelle_extra.ML\" |
83 \"$MUTABELLE_HOME/mutabelle_extra.ML\" |
84 begin |
84 begin |
85 |
85 |
|
86 declare [[quickcheck_timeout = 30]] |
|
87 |
86 ML {* |
88 ML {* |
87 val mtds = [ |
89 val mtds = [ |
88 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\", |
90 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\", |
89 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\", |
91 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\", |
90 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\", |
92 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\", |