# HG changeset patch # User traytel # Date 1376330643 -7200 # Node ID 7f7bbeb165382cf79b0581517c2c389ad8f73c31 # Parent 9e22d62642776ae41c80c1cc189c7186788644b0 eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs) diff -r 9e22d6264277 -r 7f7bbeb16538 src/HOL/BNF/BNF_Def.thy --- 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: -"\g x = g' x; x \ A\ \ x \ (Collect (split (Grp A g)))" +"x \ A \ x \ (Collect (split (Grp A g)))" unfolding convol_def Grp_def by auto definition csquare where diff -r 9e22d6264277 -r 7f7bbeb16538 src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Aug 12 15:36:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Aug 12 20:04:03 2013 +0200 @@ -111,7 +111,7 @@ rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, - rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac]) + rtac @{thm convol_mem_GrpI}, etac set_mp, atac]) set_maps]) @{thms fst_convol snd_convol} [map_id', refl])] 1 end;