diff -r f8aed3706af7 -r 799859f2e657 src/HOL/List.ML --- 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";