adding quickcheck generators in some HOL-Library theories
authorbulwahn
Tue Dec 20 17:40:18 2011 +0100 (2011-12-20)
changeset 45928874845660119
parent 45927 e0305e4f02c9
child 45929 d7d6c8cfb6f6
adding quickcheck generators in some HOL-Library theories
src/HOL/Library/Polynomial.thy
src/HOL/Library/RBT.thy
     1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Dec 20 17:40:17 2011 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Dec 20 17:40:18 2011 +0100
     1.3 @@ -1503,6 +1503,8 @@
     1.4  
     1.5  code_datatype "0::'a::zero poly" pCons
     1.6  
     1.7 +quickcheck_generator poly constructors: "0::'a::zero poly", pCons
     1.8 +
     1.9  declare pCons_0_0 [code_post]
    1.10  
    1.11  instantiation poly :: ("{zero, equal}") equal
     2.1 --- a/src/HOL/Library/RBT.thy	Tue Dec 20 17:40:17 2011 +0100
     2.2 +++ b/src/HOL/Library/RBT.thy	Tue Dec 20 17:40:18 2011 +0100
     2.3 @@ -169,5 +169,8 @@
     2.4    "distinct (keys t)"
     2.5    by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
     2.6  
     2.7 +subsection {* Quickcheck generators *}
     2.8 +
     2.9 +quickcheck_generator rbt constructors: empty, insert
    2.10  
    2.11  end