[isabelle-dev] Considered harmful: surj

[Florian Haftmann]

> 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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
>> le-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160711/c4df122c/attachment.sig>