changeset 8600 | a466c687c726 |
parent 6470 | f3015fd68d66 |
child 12218 | 6597093b77e7 |
--- a/src/HOLCF/IOA/ex/TrivEx.ML Tue Mar 28 12:28:24 2000 +0200 +++ b/src/HOLCF/IOA/ex/TrivEx.ML Tue Mar 28 17:31:36 2000 +0200 @@ -22,9 +22,8 @@ by (rtac imp_conj_lemma 1); by (simp_tac (simpset() addsimps [trans_of_def, C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); +by (induct_tac "a" 1); by (simp_tac (simpset() addsimps [h_abs_def]) 1); -by (induct_tac "a" 1); -by Auto_tac; qed"h_abs_is_abstraction";