[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Makarius]

On 11/01/18 13:20, Lawrence Paulson wrote:
>> On 10 Jan 2018, at 21:26, Makarius <makarius at 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