# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 0c071c5202b5bb630f878f3f36dd794236bfb6f8
# Parent  99a4ef20704df79e04f7d54e9c510923ea52e98c
activating construction of exhaustive testing combinators

diff -r 99a4ef20704d -r 0c071c5202b5 src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -133,9 +133,7 @@
 
 use "Tools/smallvalue_generators.ML"
 
-(* We do not activate smallcheck yet.
 setup {* Smallvalue_Generators.setup *}
-*)
 
 hide_fact orelse_def catch_match_def
 hide_const (open) orelse catch_match