e@i.P[e] == e:E. ((loc(e) = i) 
P[e])
Definitions :
all: x:A. B[x],
es-E: E,
implies: P Q,
equal: s = t,
Id: Id,
es-loc: loc(e)
FDL editor aliases :
alle-at
\mforall{}e@i.P[e] == \mforall{}e:E. ((loc(e) = i) {}\mRightarrow{} P[e])
Date html generated:
2010_08_27-AM-01_07_15
Last ObjectModification:
2008_02_27-PM-10_02_24
Home
Index