1.1 --- a/src/HOL/Meson.thy	Mon May 21 16:37:28 2012 +0200
     1.2 +++ b/src/HOL/Meson.thy	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -125,6 +125,12 @@
     1.4  lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
     1.5  by simp
     1.6  
     1.7 +lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)"
     1.8 +apply (erule contrapos_np)
     1.9 +apply clarsimp
    1.10 +apply (rule cong[where f = F])
    1.11 +by auto
    1.12 +
    1.13  
    1.14  text{* Combinator translation helpers *}
    1.15  
    1.16 @@ -198,7 +204,7 @@
    1.17  hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
    1.18      not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
    1.19      disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
    1.20 -    COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C
    1.21 -    abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
    1.22 +    ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
    1.23 +    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
    1.24  
    1.25  end