# HG changeset patch
# User paulson
# Date 903714561 -7200
# Node ID 9daf0136db6a05490473d2b1731ae5ccc956faf2
# Parent  bd539b72d4849f5e673fbcecc20407dfdc97b2fd
tidied

diff -r bd539b72d484 -r 9daf0136db6a src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Fri Aug 21 16:14:34 1998 +0200
+++ b/src/HOL/Induct/Comb.ML	Fri Aug 21 17:49:21 1998 +0200
@@ -29,16 +29,16 @@
 by (Blast_tac 1);
 by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
                           addSDs [spec_mp]) 1);
-val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
+qed_spec_mp "diamond_strip_lemmaE";
 
-val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
-by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
+Goal "diamond(r) ==> diamond(r^*)";
+by (stac diamond_def 1);  (*unfold only in goal, not in premise!*)
 by (rtac (impI RS allI RS allI) 1);
 by (etac rtrancl_induct 1);
 by (Blast_tac 1);
-by (slow_best_tac  (*Seems to be a brittle, undirected search*)
+by (best_tac  (*Seems to be a brittle, undirected search*)
     (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
-            addEs [major RS diamond_strip_lemmaE]) 1);
+            addEs [diamond_strip_lemmaE RS exE]) 1);
 qed "diamond_rtrancl";