changeset 3207 | fe79ad367d77 |
parent 2922 | 580647a879cf |
child 4089 | 96fba19bcbe2 |
--- a/src/HOL/Lambda/ParRed.ML Thu May 15 15:51:09 1997 +0200 +++ b/src/HOL/Lambda/ParRed.ML Thu May 15 15:51:47 1997 +0200 @@ -86,7 +86,7 @@ by (etac rev_mp 1); by (dB.induct_tac "dB1" 1); by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] - unsafe_addss (!simpset)))); + addss (!simpset)))); qed_spec_mp "par_beta_cd"; (*** Confluence (via cd) ***)