src/HOL/List.ML
changeset 6820 41d9b7bbf968
parent 6813 bf90f86502b2
child 6831 799859f2e657
     1.1 --- a/src/HOL/List.ML	Fri Jun 11 10:35:55 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Fri Jun 11 17:14:00 1999 +0200
     1.3 @@ -380,6 +380,16 @@
     1.4  qed "Nil_is_rev_conv";
     1.5  AddIffs [Nil_is_rev_conv];
     1.6  
     1.7 +Goal "!ys. (rev xs = rev ys) = (xs = ys)";
     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 (Asm_simp_tac 1);
    1.13 +by (Force_tac 1);
    1.14 +qed_spec_mp "rev_is_rev_conv";
    1.15 +AddIffs [rev_is_rev_conv];
    1.16 +
    1.17  val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
    1.18  by (stac (rev_rev_ident RS sym) 1);
    1.19  by (res_inst_tac [("list", "rev xs")] list.induct 1);