| changeset 6831 | 799859f2e657 |
| parent 6820 | 41d9b7bbf968 |
| child 7028 | 6ea3b385e731 |
--- a/src/HOL/List.ML Thu Jun 17 10:33:33 1999 +0200 +++ b/src/HOL/List.ML Thu Jun 17 10:33:43 1999 +0200 @@ -381,10 +381,10 @@ AddIffs [Nil_is_rev_conv]; Goal "!ys. (rev xs = rev ys) = (xs = ys)"; -by(induct_tac "xs" 1); +by (induct_tac "xs" 1); by (Force_tac 1); -br allI 1; -by(exhaust_tac "ys" 1); +by (rtac allI 1); +by (exhaust_tac "ys" 1); by (Asm_simp_tac 1); by (Force_tac 1); qed_spec_mp "rev_is_rev_conv";