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.

Tobias




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.