[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))"
from
"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.