Def spanner(f;T;to;from)
Def == (l:Edge(T). f(l) = f(inverse(l)))
Def == & (i:|T|, l1,l2:Edge(T).
Def == & ((l1  to(i))
Def == & (
Def == & ((l2  to(i))  l1 = l2  IdLnk  (f(l1))  (f(l2)))

is mentioned

In prior sections: mb event system 7

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html