# HG changeset patch # User bulwahn # Date 1319006244 -7200 # Node ID fe9993491317ef5a4ace989a32a2871287df6c53 # Parent 189c81779a683a5f96693d9911bd8cad40a428a5 removing quickcheck tester SML-inductive based on the old code generator diff -r 189c81779a68 -r fe9993491317 src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Wed Oct 19 08:37:23 2011 +0200 +++ b/src/HOL/Quickcheck.thy Wed Oct 19 08:37:24 2011 +0200 @@ -144,13 +144,6 @@ 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 *} fun iter' ::