added [simp]
authornipkow
Wed Feb 02 08:53:03 2005 +0100 (2005-02-02)
changeset 15483704b3ce6d0f7
parent 15482 b3f530e7aa1c
child 15484 2636ec211ec8
added [simp]
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 02 08:45:14 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 02 08:53:03 2005 +0100
     1.3 @@ -1828,7 +1828,7 @@
     1.4  lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
     1.5    by (unfold fold1_def) (blast intro: foldSet1_determ)
     1.6  
     1.7 -lemma fold1_singleton: "fold1 f {a} = a"
     1.8 +lemma fold1_singleton[simp]: "fold1 f {a} = a"
     1.9    by (unfold fold1_def) blast
    1.10  
    1.11  lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow>