Yes I second that. It surely is a good idea to just use it only as a input translation.
- Johannes Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann: > Hi all, > > since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f = > UNIV›. This is a little bit unfortunate since an ordinary equation is > just hidden in output that way, resulting in lots of casual > confusion. I > would suggest to turn ‹surj› into a mere input abbreviation, similar > to > ‹trivial_limit› which also covers an equality. This may also open the > possibility to re-introduce ‹surj_on f A› as in input abbreviation > for > ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange > assymmetry wrt. inj(_on), bij(_betw). > > Cheers, > Florian > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
