# HG changeset patch # User wenzelm # Date 1350566108 -7200 # Node ID b76937179ff5e97929f021b1f2bc8bbde28d34c6 # Parent c6307ee2665df5a21eb157cf6b9e0ce58fca9519 fixed proof (cf. a81f95693c68); diff -r c6307ee2665d -r b76937179ff5 src/HOL/Cardinals/Wellorder_Embedding_Base.thy --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Oct 18 14:15:46 2012 +0200 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Oct 18 15:15:08 2012 +0200 @@ -722,8 +722,8 @@ (snd o h1) y = (snd o h2) y" by auto hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \ (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)" - by (auto simp add: image_def) - thus "H h1 x = H h2 x" by (simp add: H_def) + by (auto simp add: image_def) + thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) qed (* More constant definitions: *) obtain h::"'a \ 'a' * bool" and f::"'a \ 'a'" and g::"'a \ bool"