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