# HG changeset patch
# User paulson
# Date 929608423 -7200
# Node ID 799859f2e65763e109758c72ee4bf1949f00db81
# Parent  f8aed3706af76bf12666ca4d7f1f28970cb654a9
expandshort

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