Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
activating construction of exhaustive testing combinators
authorbulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40914 0c071c5202b5
parent 40913 99a4ef20704d
child 40915 a4c956d1f91f
activating construction of exhaustive testing combinators
src/HOL/Smallcheck.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle