equal
deleted
inserted
replaced
54 only admit a purely static reading, thus being intelligible later without |
54 only admit a purely static reading, thus being intelligible later without |
55 requiring dynamic replay that is so typical for traditional proof scripts. |
55 requiring dynamic replay that is so typical for traditional proof scripts. |
56 Any of the Isabelle/Isar commands may be executed in single-steps, so |
56 Any of the Isabelle/Isar commands may be executed in single-steps, so |
57 basically the interpreter has a proof text debugger already built-in. |
57 basically the interpreter has a proof text debugger already built-in. |
58 |
58 |
59 Employing the \emph{ProofGeneral/isar} instantiation of the generic Emacs |
59 Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs |
60 interface for interactive proof assistants of LFCS Edinburgh, we arrive at a |
60 interface for interactive proof assistants of LFCS Edinburgh, we arrive at a |
61 reasonable environment for \emph{live document editing}. Thus proof texts |
61 reasonable environment for \emph{live document editing}. Thus proof texts |
62 may be developed incrementally by issuing proper document constructors, |
62 may be developed incrementally by issuing proper document constructors, |
63 including forward and backward tracing of partial documents; intermediate |
63 including forward and backward tracing of partial documents; intermediate |
64 states may be inspected by diagnostic commands. |
64 states may be inspected by diagnostic commands. |