changeset 9858 | c3ac6128b649 |
parent 9827 | ce6e22ff89c3 |
child 9906 | 5c027cca6262 |
--- 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)"