| changeset 5758 | 27a2b36efd95 |
| parent 5525 | 896f8234b864 |
| child 8423 | 3c19160b6432 |
--- a/src/HOL/Lambda/ListOrder.ML Fri Oct 23 20:36:21 1998 +0200 +++ b/src/HOL/Lambda/ListOrder.ML Fri Oct 23 20:44:34 1998 +0200 @@ -43,6 +43,7 @@ "(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \ \ ==> (ys@vs,xs@us) : step1 r"; by (Auto_tac); + by (Blast_tac 1); by (blast_tac (claset() addIs [append_eq_appendI]) 1); qed "append_step1I";