summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/isar-ref.tex

changeset 7981 | 5120a2a15d06 |

parent 7974 | 34245feb6e82 |

child 7988 | feea893b47c7 |

1.1 --- a/doc-src/IsarRef/isar-ref.tex Sat Oct 30 20:12:23 1999 +0200 1.2 +++ b/doc-src/IsarRef/isar-ref.tex Sat Oct 30 20:13:16 1999 +0200 1.3 @@ -54,14 +54,13 @@ 1.4 1.5 The current version of Isabelle offers Isar as an alternative proof language 1.6 interface layer. The Isabelle/Isar system provides an interpreter for the 1.7 - Isar formal proof document language. The input may consist either of 1.8 - \emph{proper document constructors}, or \emph{improper auxiliary commands} 1.9 - (for diagnostics, exploration etc.). Proof texts consisting of proper 1.10 - document constructors only, admit a purely static reading, thus being 1.11 - intelligible later without requiring dynamic replay that is so typical for 1.12 - traditional proof scripts. Any of the Isabelle/Isar commands may be 1.13 - executed in single-steps, so basically the interpreter has a proof text 1.14 - debugger already built-in. 1.15 + Isar formal proof document language. The input may consist either of proper 1.16 + document constructors, or improper auxiliary commands (for diagnostics, 1.17 + exploration etc.). Proof texts consisting of proper document constructors 1.18 + only, admit a purely static reading, thus being intelligible later without 1.19 + requiring dynamic replay that is so typical for traditional proof scripts. 1.20 + Any of the Isabelle/Isar commands may be executed in single-steps, so 1.21 + basically the interpreter has a proof text debugger already built-in. 1.22 1.23 Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs 1.24 interface for interactive proof assistants of LFCS Edinburgh, we arrive at a