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
