Am 19.08.2010 um 13:15 schrieb Florian Haftmann:
>> One thing I don't get: if HOL.eq is already taken, why not map the equality
>> symbol to something else?
>
> Well, eq seems more natural when looking at the traditional xsymbol
> syntax \ (although the corresponding abbreviation is named
> not
> One thing I don't get: if HOL.eq is already taken, why not map the equality
> symbol to something else?
Well, eq seems more natural when looking at the traditional xsymbol
syntax \ (although the corresponding abbreviation is named
not_equal). When using HOL.equal, there is always an uncertaint
Hi Florian,
as always, it will hurt a bit I guess, but I think it is the right thing to do.
Cheers,
Gerwin
On 19/08/2010, at 11:18 AM, Florian Haftmann wrote:
> Hi all,
>
> with authentic syntax being default and thanks to antiquotations, we
> have now reached a state where we could replace al
Your proposal makes sense to me. Naturally it should be announced on the
mailing list so that our users have ample warning.
One thing I don't get: if HOL.eq is already taken, why not map the equality
symbol to something else?
Larry
On 19 Aug 2010, at 11:18, Florian Haftmann wrote:
> a) Applica
Hi all,
with authentic syntax being default and thanks to antiquotations, we
have now reached a state where we could replace all the remaining
unqualified symbol names in HOL.thy (between "global" and "local").
While this should be technically quite easy, there remain two open
questions before pro
