# HG changeset patch
# User krauss
# Date 1184613432 -7200
# Node ID cfe8d4bf749a32fa9e3b7a3942617bad52649d73
# Parent  ee3ee9ea0d34a008ce84128e8b2400dbe672fdff
added lemma binding: accpI = accp.accI

diff -r ee3ee9ea0d34 -r cfe8d4bf749a src/HOL/Accessible_Part.thy
--- 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 *}