Re: [isabelle] what the meaning of the set's operation `` ?



 wrote:
> The following are the part of context in dfs.thy.
> ----------------------------------------------------------------
> subsection "Definition of Graphs"
> typedecl node 
> types graph = "(node * node) list"
> consts
>   nexts :: "[graph, node] \<Rightarrow> node list"
> primrec
>   "nexts [] n = []"
>   "nexts (e#es) n = (if fst e = n then snd e # nexts es n else nexts es n)"
> definition
>   nextss :: "[graph, node list] \<Rightarrow> node set" where
>   "nextss g xs = set g `` set xs"
> -----------------------------------------------------------------------
> I don't know the meaning of the operation `` in the "nextss g xs = set g `` set xs"?
>                                                        yucy
>   
The infix `` is the image of a relation over a set. It is defined in
Relation.thy.

Regards
Tobias






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