# HG changeset patch
# User nipkow
# Date 1107330783 -3600
# Node ID 704b3ce6d0f77abee09afa772974674a586a4080
# Parent  b3f530e7aa1c92497dbb1b398cac11814256a39d
added [simp]

diff -r b3f530e7aa1c -r 704b3ce6d0f7 src/HOL/Finite_Set.thy
--- 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>