# HG changeset patch
# User nipkow
# Date 804415387 -7200
# Node ID 1831ba01c90c1bbaace21eb34572e05041dd0647
# Parent  8845eb5f0e5ec2458e788357077903b2e0173cb1
Minimal proof tuning.

diff -r 8845eb5f0e5e -r 1831ba01c90c src/HOL/Lambda/Confluence.ML
--- a/src/HOL/Lambda/Confluence.ML	Mon Jun 26 14:34:19 1995 +0200
+++ b/src/HOL/Lambda/Confluence.ML	Thu Jun 29 10:43:07 1995 +0200
@@ -37,15 +37,10 @@
 goalw Confluence.thy [confluent_def,diamond_def,Church_Rosser_def]
   "Church_Rosser(R) = confluent(R)";
 br iffI 1;
- by(safe_tac HOL_cs);
- be allE 1;
- be allE 1;
- be mp 1;
- br rtrancl_trans 1;
-  br (Un_upper2 RS rtrancl_mono RS subsetD) 1;
-  br rtrancl_converseI 1;
-  be converseI 1;
- be (Un_upper1 RS rtrancl_mono RS subsetD) 1;
+ by(fast_tac (HOL_cs addIs
+      [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
+       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
+by(safe_tac HOL_cs);
 be rtrancl_induct 1;
  by(fast_tac trancl_cs 1);
  by(slow_tac (rel_cs addIs [r_into_rtrancl]