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.
more convenient order of code equations
authorhaftmann
Wed, 26 May 2010 11:59:06 +0200
changeset 37123 9cce71cd4bf0
parent 37121 8e51fc35d59f
child 37124 fe22fc54b876
child 37135 636e6d8645d6
more convenient order of code equations
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle