For sure. I think it confuses beginners at first, because == is only allowed in "real" definitions rather than derived ones. Larry
On 3 Sep 2013, at 00:39, Gerwin Klein <[email protected]> wrote: > I also still use == quite a bit, I never understood why it is discouraged so > much. It has the better precedence, and I use it mostly for the difference > between a definition and an equation, which non-Isabelle people seem to > understand. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
