> Yes I second that. It surely is a good idea to just use it only as a > input translation.
See now 6af79184bef3.
Florian
>
> - 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
>
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
