Lines Matching defs:old
2742 {\it old\_thms\/} is a list of theorems concerning the lower, representative
2748 lifted versions of the {\it old\_thms}.
2752 record with the same fields as above except for {\it old\_thms},
2755 is then used to lift the old theorems individually, one at a time.
3173 are lists of theorems. The last field ({\tt old\_thms})
3201 respectfulness of all constants used in {\tt old\_thms}
4235 \subsection{Theorems to be lifted: {\tt old\_thms}}
4240 {\tt old\_thms} are the theorems to be lifted. They should involve only
5361 The old theorems to be lifted are too many to list, but some will
5535 % old:
5571 % old:
5632 % old: