Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped superfluous if
authorhaftmann
Tue, 07 Oct 2008 16:07:20 +0200
changeset 28515 b26ba1b1dbda
parent 28514 da83a614c454
child 28516 e6fdcaaadbd3
dropped superfluous if
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle