src/HOL/Meson.thy
changeset 47953 a2c3706c4cb1
parent 42616 92715b528e78
child 48891 c0eafbd55de3
--- a/src/HOL/Meson.thy	Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Meson.thy	Tue May 22 16:59:27 2012 +0200
@@ -125,6 +125,12 @@
 lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
 by simp
 
+lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)"
+apply (erule contrapos_np)
+apply clarsimp
+apply (rule cong[where f = F])
+by auto
+
 
 text{* Combinator translation helpers *}
 
@@ -198,7 +204,7 @@
 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
     not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
     disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
-    COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C
-    abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
+    ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
+    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
 
 end