# HG changeset patch
# User paulson
# Date 831635024 -7200
# Node ID 35961ebbbfad5558db3b8cea6220969b2afcfc2c
# Parent  a70a5bc5e3153e2c71fef0fd4dd4e0c40b3807a1
Added prune_params_tac to improve readability of subgoals

diff -r a70a5bc5e315 -r 35961ebbbfad src/HOL/ex/Comb.ML
--- a/src/HOL/ex/Comb.ML	Wed May 08 18:01:54 1996 +0200
+++ b/src/HOL/ex/Comb.ML	Thu May 09 11:43:44 1996 +0200
@@ -133,7 +133,7 @@
 (*Church-Rosser property for parallel contraction*)
 goalw Comb.thy [diamond_def] "diamond(parcontract)";
 by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract.induct 1);
+by (etac parcontract.induct 1 THEN prune_params_tac);
 by (ALLGOALS 
     (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
 qed "diamond_parcontract";
@@ -163,7 +163,7 @@
 goal Comb.thy "parcontract <= contract^*";
 by (rtac subsetI 1);
 by (split_all_tac 1);
-by (etac parcontract.induct 1);
+by (etac parcontract.induct 1 THEN prune_params_tac);
 by (ALLGOALS (deepen_tac reduce_cs 0));
 qed "parcontract_subset_reduce";