| changeset 52986 | 7f7bbeb16538 |
| parent 52749 | ed416f4ac34e |
| child 53560 | 4b5f42cfa244 |
--- a/src/HOL/BNF/BNF_Def.thy Mon Aug 12 15:36:55 2013 +0200 +++ b/src/HOL/BNF/BNF_Def.thy Mon Aug 12 20:04:03 2013 +0200 @@ -31,7 +31,7 @@ unfolding convol_def by simp lemma convol_mem_GrpI: -"\<lbrakk>g x = g' x; x \<in> A\<rbrakk> \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))" +"x \<in> A \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))" unfolding convol_def Grp_def by auto definition csquare where