| changeset 15481 | fc075ae929e4 |
| parent 13798 | 4c1a53627500 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/UNITY/ListOrder.thy Sun Jan 30 20:48:50 2005 +0100 +++ b/src/HOL/UNITY/ListOrder.thy Tue Feb 01 18:01:57 2005 +0100 @@ -215,8 +215,7 @@ apply (erule disjE) apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append) apply (blast intro: genPrefix.append, auto) -apply (subst append_cons_eq) -apply (blast intro: genPrefix_append_both genPrefix.append) +apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append) done lemma append_one_genPrefix: