removing instantiation exhaustive for unit in Quickcheck_Exhaustive
authorbulwahn
Thu Apr 07 14:51:26 2011 +0200 (2011-04-07)
changeset 4227450850486f8dc
parent 42273 3b94cbd903c1
child 42275 79be89e07589
removing instantiation exhaustive for unit in Quickcheck_Exhaustive
src/HOL/Quickcheck_Exhaustive.thy
     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