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
  Peter Lammich



> P is another type. I am confused about the syntax of the finite set in
> HOL.
>
> In list would be something like:
>
> ALL (B :: name list) P.
>
> Thanks in advance for any help.
>
> -T






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