(This is just a side-track on HOL notation, which came to me when cleaning
up theories with old ASCII replacement syntax like & | --> <-> Un Int etc.
-- which is very easy with explicit C+b completion in Isabelle/jEdit.)
Isabelle/4379d46c8e13 (Oct 2005) introduces "alternative iff syntax for
equality on booleans, with print_mode 'iff'".
I can't remember a particular reason for the print mode, instead of having
that syntax always on. I find myself using the "iff" notation most of the
time to make theories look "nice".
Are there clubs of "iff" vs. "non-iff"? If almost everybody is a member
of the "iff" club we could just remove that print mode. (We don't have to
consider that for the coming release, to avoid any real-time pressure on
this question.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
