| changeset 3724 | f33e301a89f5 |
| parent 3207 | fe79ad367d77 |
| child 4089 | 96fba19bcbe2 |
--- a/src/HOL/Induct/Comb.ML Mon Sep 29 11:36:44 1997 +0200 +++ b/src/HOL/Induct/Comb.ML Mon Sep 29 11:37:02 1997 +0200 @@ -130,7 +130,7 @@ goalw Comb.thy [diamond_def] "diamond parcontract"; by (rtac (impI RS allI RS allI) 1); by (etac parcontract.induct 1 THEN prune_params_tac); -by (Step_tac 1); +by Safe_tac; by (ALLGOALS Blast_tac); qed "diamond_parcontract";