author | wenzelm |
Tue, 05 Sep 2000 18:49:02 +0200 | |
changeset 9858 | c3ac6128b649 |
parent 9857 | 2f994c499bef |
child 9859 | 2cd338998b53 |
--- 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)"