eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
authortraytel
Mon Aug 12 20:04:03 2013 +0200 (2013-08-12)
changeset 529867f7bbeb16538
parent 52985 9e22d6264277
child 52987 b44a11b87b85
eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/Tools/bnf_def_tactics.ML
     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
     2.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Aug 12 15:36:55 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Aug 12 20:04:03 2013 +0200
     2.3 @@ -111,7 +111,7 @@
     2.4              rtac CollectI,
     2.5              CONJ_WRAP' (fn thm =>
     2.6                EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
     2.7 -                rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac])
     2.8 +                rtac @{thm convol_mem_GrpI}, etac set_mp, atac])
     2.9              set_maps])
    2.10            @{thms fst_convol snd_convol} [map_id', refl])] 1
    2.11    end;