--- a/src/HOL/Enum.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Enum.thy Sun Nov 10 15:05:06 2013 +0100
@@ -178,13 +178,9 @@
lemma [code]:
fixes xs :: "('a::finite \<times> 'a) list"
- shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
+ shows "Wellfounded.acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
by (simp add: card_UNIV_def acc_bacc_eq)
-lemma [code]:
- "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
- by (simp add: acc_def)
-
subsection {* Default instances for @{class enum} *}