equal
deleted
inserted
replaced
74 \medskip |
74 \medskip |
75 |
75 |
76 Occasionally, a user's \texttt{.emacs} contains material that is incompatible |
76 Occasionally, a user's \texttt{.emacs} contains material that is incompatible |
77 with the version of (X)Emacs that Proof~General prefers. Then proper startup |
77 with the version of (X)Emacs that Proof~General prefers. Then proper startup |
78 may be still achieved by using the \texttt{-u false} option.\footnote{Any |
78 may be still achieved by using the \texttt{-u false} option.\footnote{Any |
79 Emacs lisp file \url{proofgeneral-settings.el} occurring in |
79 Emacs lisp file \texttt{proofgeneral-settings.el} occurring in |
80 \url{$ISABELLE_HOME/etc} or \url{$ISABELLE_HOME_USER/etc} is automatically |
80 \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is |
81 loaded by the Proof~General interface script as well.} |
81 automatically loaded by the Proof~General interface script as well.} |
82 |
82 |
83 \section{How to write Isar proofs anyway?} |
83 \section{How to write Isar proofs anyway?} |
84 |
84 |
85 This is one of the key questions, of course. Isar offers a rather different |
85 This is one of the key questions, of course. Isar offers a rather different |
86 approach to formal proof documents than plain old tactic scripts. Experienced |
86 approach to formal proof documents than plain old tactic scripts. Experienced |