src/HOL/Quickcheck_Exhaustive.thy
changeset 42274 50850486f8dc
parent 42230 594480d25aaa
child 42304 34366f39d32d
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 07 14:51:25 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 07 14:51:26 2011 +0200
     1.3 @@ -18,15 +18,6 @@
     1.4  class exhaustive = term_of +
     1.5  fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.6  
     1.7 -instantiation unit :: exhaustive
     1.8 -begin
     1.9 -
    1.10 -definition "exhaustive f d = f (Code_Evaluation.valtermify ())"
    1.11 -
    1.12 -instance ..
    1.13 -
    1.14 -end
    1.15 -
    1.16  instantiation code_numeral :: exhaustive
    1.17  begin
    1.18