changeset 49753 | a344f1a21211 |
parent 49310 | 6e30078de4f0 |
child 49922 | b76937179ff5 |
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 15:01:20 2012 +0200 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 15:17:40 2012 +0200 @@ -273,7 +273,7 @@ lemma embed_underS: -assumes WELL: "Well_order r" and WELL: "Well_order r'" and +assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r r' f" and IN: "a \<in> Field r" shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))" proof-