expandshort

--- 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";