# HG changeset patch
# User wenzelm
# Date 968172542 -7200
# Node ID c3ac6128b649eaa1ef3d6c326e81f2627354c612
# Parent  2f994c499bef4cff4f910ea4fccf239eef70bb34
use 'iff' modifier;

diff -r 2f994c499bef -r c3ac6128b649 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Tue Sep 05 18:48:41 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy	Tue Sep 05 18:49:02 2000 +0200
@@ -176,7 +176,7 @@
     apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
    apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
   apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
-    other: dB.distinct [iff del, simp])    (*23 seconds?*)
+    iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   done
 
 lemma confluent_beta_eta: "confluent (beta \<union> eta)"