Re: [isabelle] Symmetric Difference of sets



I recommend not to make it a definition but an abbreviation, which saves
you having to prove intro and elim rules and instrument the automatic
provers.

Tobias

Iain Whiteside wrote:
> Hi All,
> 
> I was looking for the symmetric difference operation on sets in Isabelle/HOL, but couldn't find it in Set.thy. Does anyone know if it exists anywhere else? I thought I'd better check before I go ahead and define it myself.
> 
> Thanks,
> 
> Iain






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