Re: [isabelle] Modifying Isabelle/ZF core?
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?
we'll certainly take contributions.
This archive was generated by a fusion of
Pipermail (Mailman edition) and