author | paulson |
Wed, 03 Mar 1999 11:27:10 +0100 | |
changeset 6303 | 5e0b1ad1a447 |
parent 6302 | 957d8e203be1 |
child 6304 | 9a82e1c3d9da |
--- a/src/HOL/W0/Type.ML Wed Mar 03 11:26:36 1999 +0100 +++ b/src/HOL/W0/Type.ML Wed Mar 03 11:27:10 1999 +0100 @@ -212,7 +212,7 @@ Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; by (simp_tac (simpset() addsimps [new_tv_list]) 1); by (induct_tac "ts" 1); -by (Safe_tac); +by Safe_tac; by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); qed_spec_mp "new_tv_subst_tel"; Addsimps [new_tv_subst_tel];