# HG changeset patch
# User haftmann
# Date 1274867946 -7200
# Node ID 9cce71cd4bf0812e132a39581c91fa14120eccb4
# Parent  8e51fc35d59f2e7b7b8158f77ed9b76ec9277795
more convenient order of code equations

diff -r 8e51fc35d59f -r 9cce71cd4bf0 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 25 23:03:13 2010 +0200
+++ b/src/HOL/List.thy	Wed May 26 11:59:06 2010 +0200
@@ -4647,8 +4647,8 @@
 lemmas in_set_code [code_unfold] = mem_iff [symmetric]
 
 lemma member_simps [simp, code]:
+  "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
   "member [] y \<longleftrightarrow> False"
-  "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
   by (auto simp add: mem_iff)
 
 lemma member_set: