src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Nov 10 15:05:06 2013 +0100
@@ -482,6 +482,11 @@
 
 lemmas accpI = accp.accI
 
+lemma accp_eq_acc [code]:
+  "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
+  by (simp add: acc_def)
+
+
 text {* Induction rules *}
 
 theorem accp_induct:
@@ -855,4 +860,7 @@
 
 declare "prod.size" [no_atp]
 
+
+hide_const (open) acc accp
+
 end