Re: [isabelle] the hereditarily finite sets

Thanks, but I believe that you are describing finite sets rather than hereditarily finite sets. I should have mentioned, the membership function should have the following type:

	member  :: hf => hf => bool

That is, we have one single type rather than separate types of sets and elements.

It sounds like this hasn't been formalised before...?


On 25 Mar 2012, at 20:18, Andreas Lochbihler wrote:

> Hi Larry,
> The FinFun formalisation in the AFP contains until Isabelle2011-1 defines such a type in theory FinFunSet. Adapting it to the pred/set-distinction, I recently (ID b7aa87989f3a) changed it from sets to predicates, so it is called FinFunPred in the development branch of the AFP.

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