changeset 5192 | 704dd3a6d47d |
parent 5132 | 24f992a25adc |
--- a/src/HOLCF/IOA/meta_theory/TrivEx.ML Fri Jul 24 13:39:47 1998 +0200 +++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML Fri Jul 24 13:44:27 1998 +0200 @@ -23,7 +23,7 @@ by (simp_tac (simpset() addsimps [trans_of_def, C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); by (simp_tac (simpset() addsimps [h_abs_def]) 1); -by (action.induct_tac "a" 1); +by (induct_tac "a" 1); by Auto_tac; qed"h_abs_is_abstraction";