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.


isabelle-dev mailing list

Reply via email to