Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)

is mentioned by

Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top.  || f	[fpf-empty-compatible-left]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top. f ||	[fpf-empty-compatible-right]
Def M1 || M2 Def == M1 ||decl M2 Def == & 1of(2of(2of(M1))) || 1of(2of(2of(M2))) Def == & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2)))) Def == & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2))))) Def == & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2)))))) Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of( Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(M2))))))) Def == & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & 1of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-compatible]
Def M1 ||decl M2 == 1of(M1) || 1of(M2) & 1of(2of(M1)) || 1of(2of(M2))	[ma-compatible-decls]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html