--- a/src/HOL/Accessible_Part.thy Mon Jul 16 21:16:16 2007 +0200
+++ b/src/HOL/Accessible_Part.thy Mon Jul 16 21:17:12 2007 +0200
@@ -31,6 +31,7 @@
termi :: "('a * 'a) set => 'a set" where
"termi r == acc (r\<inverse>)"
+lemmas accpI = accp.accI
subsection {* Induction rules *}