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.
added [simp]
authornipkow
Wed, 02 Feb 2005 08:53:03 +0100
changeset 15483 704b3ce6d0f7
parent 15482 b3f530e7aa1c
child 15484 2636ec211ec8
added [simp]
src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite_Set.thy	Wed Feb 02 08:45:14 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 02 08:53:03 2005 +0100
@@ -1828,7 +1828,7 @@
 lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
   by (unfold fold1_def) (blast intro: foldSet1_determ)
 
-lemma fold1_singleton: "fold1 f {a} = a"
+lemma fold1_singleton[simp]: "fold1 f {a} = a"
   by (unfold fold1_def) blast
 
 lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow>
isabelle