src/HOL/Enum.thy
changeset 54295 45a5523d4a63
parent 54148 c8cc5ab4a863
child 54890 cb892d835803
     1.1 --- a/src/HOL/Enum.thy	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/src/HOL/Enum.thy	Sun Nov 10 15:05:06 2013 +0100
     1.3 @@ -178,13 +178,9 @@
     1.4  
     1.5  lemma [code]:
     1.6    fixes xs :: "('a::finite \<times> 'a) list"
     1.7 -  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
     1.8 +  shows "Wellfounded.acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
     1.9    by (simp add: card_UNIV_def acc_bacc_eq)
    1.10  
    1.11 -lemma [code]:
    1.12 -  "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
    1.13 -  by (simp add: acc_def)
    1.14 -
    1.15  
    1.16  subsection {* Default instances for @{class enum} *}
    1.17