src/HOL/Finite_Set.thy
changeset 15483 704b3ce6d0f7
parent 15480 cb3612cc41a3
child 15484 2636ec211ec8
--- 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>