diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Quickcheck.thy Mon Oct 17 10:19:01 2011 +0200 @@ -144,6 +144,12 @@ no_notation fcomp (infixl "\>" 60) no_notation scomp (infixl "\\" 60) +subsection {* Tester SML-inductive based on the SML code generator *} + +setup {* + Context.theory_map (Quickcheck.add_tester ("SML_inductive", + (Inductive_Codegen.active, Quickcheck_Common.generator_test_goal_terms Inductive_Codegen.test_term))); +*} subsection {* The Random-Predicate Monad *}