expandshort
authorpaulson
Thu Jun 17 10:33:43 1999 +0200 (1999-06-17)
changeset 6831799859f2e657
parent 6830 f8aed3706af7
child 6832 0c92ccb3c4ba
expandshort
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Thu Jun 17 10:33:33 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Jun 17 10:33:43 1999 +0200
     1.3 @@ -381,10 +381,10 @@
     1.4  AddIffs [Nil_is_rev_conv];
     1.5  
     1.6  Goal "!ys. (rev xs = rev ys) = (xs = ys)";
     1.7 -by(induct_tac "xs" 1);
     1.8 +by (induct_tac "xs" 1);
     1.9   by (Force_tac 1);
    1.10 -br allI 1;
    1.11 -by(exhaust_tac "ys" 1);
    1.12 +by (rtac allI 1);
    1.13 +by (exhaust_tac "ys" 1);
    1.14   by (Asm_simp_tac 1);
    1.15  by (Force_tac 1);
    1.16  qed_spec_mp "rev_is_rev_conv";