changeset 216 | 4a10bc05210a |
parent 8 | c3d2c6dcf3f0 |
child 290 | 37d580c16af5 |
--- a/src/CCL/ex/stream.ML Wed Jan 05 19:41:37 1994 +0100 +++ b/src/CCL/ex/stream.ML Wed Jan 05 19:43:46 1994 +0100 @@ -108,7 +108,6 @@ by (fast_tac (type_cs addSIs [napplyBzero RS sym, napplyBzero RS sym RS arg_cong]) 1); by (EQgen_tac list_ss [iter1B,iter2Blemma] 1); -by (assume_tac 1); (*should EQgen_tac call asm_simp_tac?*) by (rtac (napply_f RS ssubst) 1 THEN atac 1); by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1); by (fast_tac type_cs 1);