# HG changeset patch
# User wenzelm
# Date 977608261 -3600
# Node ID 66604af28f945498c817dca70c99e1fb8e2c778e
# Parent  59f82484e00058870eaaa67f9bc89b6612eb6c20
tuned;

diff -r 59f82484e000 -r 66604af28f94 src/HOL/Library/Accessible_Part.thy
--- a/src/HOL/Library/Accessible_Part.thy	Sat Dec 23 22:50:39 2000 +0100
+++ b/src/HOL/Library/Accessible_Part.thy	Sat Dec 23 22:51:01 2000 +0100
@@ -23,7 +23,7 @@
   acc :: "('a \<times> 'a) set => 'a set"
 inductive "acc r"
   intros
-    accI [rule_format]: "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
+    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
 
 syntax
   termi :: "('a \<times> 'a) set => 'a set"
@@ -33,7 +33,7 @@
 
 subsection {* Induction rules *}
 
-theorem acc_induct [induct set: acc]:
+theorem acc_induct:
   "a \<in> acc r ==>
     (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
 proof -
@@ -48,6 +48,8 @@
     done
 qed
 
+theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
+
 theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
   apply (erule acc.elims)
   apply fast