[isabelle] finite set syntax

Hi all,

Is there a way to have a quantification over a finite set of names; something like

ALL (finite name  B) P.

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.


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