| changeset 17955 | 3b34516662c6 |
| parent 17233 | 41eee2e7b465 |
| child 19360 | f47412f922ab |
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Oct 21 16:34:22 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Oct 21 18:14:32 2005 +0200 @@ -161,7 +161,7 @@ by (pair_induct_tac "xs" [is_exec_frag_def] 1); (* main case *) -ren "ss a t" 1; +by (rename_tac "ss a t" 1); by (safe_tac set_cs); by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1)); qed"lemma_1_1a";