# HG changeset patch # User wenzelm # Date 936720544 -7200 # Node ID c8b5dcacf2e37e585939849d760e7b62bfd69ab3 # Parent e70255cb10356f834bc65a16612dd4f10f5fb058 \url; diff -r e70255cb1035 -r c8b5dcacf2e3 doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Tue Sep 07 18:08:51 1999 +0200 +++ b/doc-src/IsarRef/intro.tex Tue Sep 07 18:09:04 1999 +0200 @@ -54,7 +54,7 @@ (default Scratch.thy). PROOFGENERAL_OPTIONS= -\end{ttbox} +\end{ttbox} %$ Apart from the command line, the defaults for these options may be overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU Emacs may be configured as follows: @@ -76,9 +76,9 @@ Occasionally, a user's \texttt{.emacs} contains material that is incompatible with the version of (X)Emacs that Proof~General prefers. Then proper startup may be still achieved by using the \texttt{-u false} option.\footnote{Any - \texttt{proofgeneral-settings.el} file occurring in - \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is - automatically loaded by the Proof~General interface script as well.} + Emacs lisp file \url{proofgeneral-settings.el} occurring in + \url{$ISABELLE_HOME/etc} or \url{$ISABELLE_HOME_USER/etc} is automatically + loaded by the Proof~General interface script as well.} \section{How to write Isar proofs anyway?}