Re: [isabelle] Isar syntax question
On 17/07/2014 00:49, Vadim Zaliva wrote:
> I do not know what is involved implementation-wiser but it would be nice if Isabelle could deal with
> trivial double negation during unification.
I have often toyed with the idea of unification modulo certain equations but
implementation-wise it is subtle and means modifying an already convoluted part
of the core. Don't hold your breath.
This archive was generated by a fusion of
Pipermail (Mailman edition) and