# HG changeset patch
# User paulson
# Date 875525804 -7200
# Node ID 034f0f5ca43fd148fcbd8124a6079a650904c8f3
# Parent  24af9e73451e76ad5cc493ea7d23dfa3d65f61a4
Tidied proof of r_comp_rtrancl_eq

diff -r 24af9e73451e -r 034f0f5ca43f src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Mon Sep 29 11:32:25 1997 +0200
+++ b/src/HOL/Trancl.ML	Mon Sep 29 11:36:44 1997 +0200
@@ -195,9 +195,8 @@
 qed "rtranclE2";
 
 goal Trancl.thy "r O r^* = r^* O r";
-by (Step_tac 1);
- by (blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
-by (blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
+by (blast_tac (!claset addEs [rtranclE, rtranclE2] 
+	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
 qed "r_comp_rtrancl_eq";