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



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





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