From c68d182951b477edeb95d71942e97cecef627d5d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz G(F(a)). Use "GFa" if you really want
to refer to GFa as a proposition.
Conversely, infix
letter operators are not assumed to be operators if they are part of
an identifier: aUb is an atomic proposition, unlike
-a U b and (a)U(b)
a U b and (a)U(b).
|
|