doc-src/Ref/introduction.tex
changeset 149 caa7a52ff46f
parent 141 a133921366cb
child 158 c2fcb6c07689
equal deleted inserted replaced
148:67d046de093e 149:caa7a52ff46f
    37 the latter course uses much less disc space.  Note that a Poly/\ML{}
    37 the latter course uses much less disc space.  Note that a Poly/\ML{}
    38 database {\bf does not} save the contents of references, such as the
    38 database {\bf does not} save the contents of references, such as the
    39 current state of a backward proof.
    39 current state of a backward proof.
    40 
    40 
    41 \item With New Jersey \ML{} you must save the state explicitly before
    41 \item With New Jersey \ML{} you must save the state explicitly before
    42 ending the session.  While Poly/\ML{} database can be small, a New Jersey
    42 ending the session.  While a Poly/\ML{} database can be small, a New Jersey
    43 image occupies several megabytes.
    43 image occupies several megabytes.
    44 \end{itemize}
    44 \end{itemize}
    45 See your \ML{} compiler's documentation for full instructions on saving the
    45 See your \ML{} compiler's documentation for full instructions on saving the
    46 state.
    46 state.
    47 
    47