src/HOL/HOL.thy
changeset 31172 74d72ba262fb
parent 31156 90fed3d4430f
child 31173 bbe9e29b9672
     1.1 --- a/src/HOL/HOL.thy	Sat May 16 10:19:01 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat May 16 15:23:52 2009 +0200
     1.3 @@ -1988,6 +1988,18 @@
     1.4  
     1.5  subsubsection {* Quickcheck *}
     1.6  
     1.7 +ML {*
     1.8 +structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
     1.9 +(
    1.10 +  val name = "quickcheck_recfun_simp"
    1.11 +  val description = "simplification rules of recursive functions as needed by Quickcheck"
    1.12 +)
    1.13 +*}
    1.14 +
    1.15 +setup {*
    1.16 +  Quickcheck_RecFun_Simp_Thms.setup
    1.17 +*}
    1.18 +
    1.19  setup {*
    1.20    Quickcheck.add_generator ("SML", Codegen.test_term)
    1.21  *}