# HG changeset patch
# User haftmann
# Date 1223388440 -7200
# Node ID b26ba1b1dbda881585a7223a6b94f59aac1964ee
# Parent  da83a614c454cfec29e434f12e7726a6270d982f
dropped superfluous if

diff -r da83a614c454 -r b26ba1b1dbda src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 07 16:07:18 2008 +0200
+++ b/src/HOL/List.thy	Tue Oct 07 16:07:20 2008 +0200
@@ -3661,7 +3661,7 @@
   member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
 where 
   "x mem [] \<longleftrightarrow> False"
-  | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
+  | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
 
 primrec
   null:: "'a list \<Rightarrow> bool"