Lines Matching refs:same
245 is the result of performing the same substitution across all of the
283 \PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, since \HOL{} was
286 the same as the corresponding rule in \LCF; the code implementing this
399 The theory \theory{LOG} has the same type
893 constant $\con{c}_i$ must be the same as the type of the corresponding
1066 the introduced constants have, via their types, the same dependency on
1068 situation is the same as that discussed in the Remark in
1307 provides one way of achieving this while at the same time preserving
1501 $q$ in $M'$ are the same as in $M$, since these expressions do not
1571 and any two models of the extended theory which restrict to the same