summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 17 Mar 2000 22:51:24 +0100 | |

changeset 8509 | daec9cef376d |

parent 8508 | 76d8d8aab881 |

child 8510 | 863bc8086f62 |

tuned;

--- a/doc-src/IsarRef/isar-ref.tex Fri Mar 17 22:51:05 2000 +0100 +++ b/doc-src/IsarRef/isar-ref.tex Fri Mar 17 22:51:24 2000 +0100 @@ -33,7 +33,7 @@ \renewcommand{\phi}{\varphi} -%\includeonly{refcard} +\includeonly{refcard} @@ -62,12 +62,12 @@ Any of the Isabelle/Isar commands may be executed in single-steps, so basically the interpreter has a proof text debugger already built-in. - Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs - interface for interactive proof assistants of LFCS Edinburgh, we arrive at a - reasonable environment for \emph{live document editing}. Thus proof texts - may be developed incrementally by issuing proper document constructors, - including forward and backward tracing of partial documents; intermediate - states may be inspected by diagnostic commands. + Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs + interface for interactive proof assistants, we arrive at a reasonable + environment for \emph{live document editing}. Thus proof texts may be + developed incrementally by issuing proper document constructors, including + forward and backward tracing of partial documents; intermediate states may + be inspected by diagnostic commands. The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc.\ may be used