rev=rev lemma.

--- a/src/HOL/List.ML	Fri Jun 11 10:35:55 1999 +0200
+++ b/src/HOL/List.ML	Fri Jun 11 17:14:00 1999 +0200
@@ -380,6 +380,16 @@
 qed "Nil_is_rev_conv";
 AddIffs [Nil_is_rev_conv];
 
+Goal "!ys. (rev xs = rev ys) = (xs = ys)";
+by(induct_tac "xs" 1);
+ by (Force_tac 1);
+br allI 1;
+by(exhaust_tac "ys" 1);
+ by (Asm_simp_tac 1);
+by (Force_tac 1);
+qed_spec_mp "rev_is_rev_conv";
+AddIffs [rev_is_rev_conv];
+
 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
 by (stac (rev_rev_ident RS sym) 1);
 by (res_inst_tac [("list", "rev xs")] list.induct 1);