| changeset 7229 | 6773ba0c36d5 |
| parent 5068 | fb28eaa07e01 |
| child 10835 | f4745d77e620 |
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Tue Aug 17 14:01:39 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Tue Aug 17 15:59:32 1999 +0200 @@ -110,7 +110,7 @@ \ andalso (stutter2 sig`xs) (snd at))"; by (rtac trans 1); by (stac stutter2_unfold 1); -by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1); +by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1); by (Simp_tac 1); qed"stutter2_cons";