[isabelle] Modifying Isabelle/ZF core?

I am writing my first theory.
Sadly I have not found in Perm.thy a theorem which would prove (given sets "small" and "big")
"embed: inj(small, range(embed))" and/or "embed: bij(small, range(embed))"
"embded: inj(small, big)"
What us to do with this theorem? Should I prove it as a lemma in my own theory? Should we modify Isabelle/ZF core to add that new theorem?
Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.