To me, the ability to use = (on booleans) as an alternative to <-> is an artefact of HOL, rather than something to encourage. Almost always, <-> is more readable. At least that's my view.
Larry On 2 Sep 2013, at 19:42, Florian Haftmann <[email protected]> wrote: >> 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.) > > I am definitely a member of the iff-club. Partly for precedence > reasons, but also because you can recognize predicate equations immediately. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
