On 11/01/18 13:20, Lawrence Paulson wrote: >> On 10 Jan 2018, at 21:26, Makarius <makar...@sketis.net> wrote: > > Interactive theorem proving isn't the same thing as solving physics problems > by hand, so I'm not against having operators at the end of the line if that's > what people think would be best. Note however that the equals sign is an > infix operator and is invariably put at the start of a line, never at the end.
The Lamport paper "How to write a long formula" seems to have such an informal context of "physics problems" by hand. What is also interesting: He does not have a good plan for implication (==>): We still have that pending problem for printing goal states, but the approach in the pipeline is to use Isar notation (fixes/assumes/shows or shows/if/for). Anyway, the "infix" annotations are just a macro on top of more general mixfix syntax. If there is sufficient demand for variations, we can provide extra macros, e.g. "infix_line", "infixl_line", "infixr_line" (or with better names). There is no need to switch back and forth all infix syntax every 10-20 years or so. If we manage without variations: the simpler the better. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev