Re: [isabelle] finite set syntax
Temesghen Kahsai wrote:
> Hi all,
> Is there a way to have a quantification over a finite set of names;
> something like
> ALL (finite name B) P.
Not really sure if I got your point, but
ALL B . finite B --> P
would do the job for finite sets B.
Hope it helped
> P is another type. I am confused about the syntax of the finite set in
> In list would be something like:
> ALL (B :: name list) P.
> Thanks in advance for any help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and