--- a/src/HOL/List.thy Thu Apr 28 12:02:49 2005 +0200
+++ b/src/HOL/List.thy Thu Apr 28 12:04:34 2005 +0200
@@ -566,12 +566,21 @@
lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
by (induct xs) auto
+lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
+by auto
+
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
by (induct xs) auto
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
by (induct xs) auto
+lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
+by (cases xs) auto
+
+lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
+by (cases xs) auto
+
lemma rev_is_rev_conv [iff]: "!!ys. (rev xs = rev ys) = (xs = ys)"
apply (induct xs, force)
apply (case_tac ys, simp, force)