aboutsummaryrefslogtreecommitdiff
path: root/html/projects/outline.html
diff options
context:
space:
mode:
authorDavid Aspinall2004-02-07 19:31:13 +0000
committerDavid Aspinall2004-02-07 19:31:13 +0000
commitb9caaa8e4b66817dbc66d0e79b567b3285869fea (patch)
treec5420dac1aa1afc28168867ca5cc9c610a46399e /html/projects/outline.html
parent87174e13a8aa064f6d00ef9248da9938ea4978f6 (diff)
Deleted file
Diffstat (limited to 'html/projects/outline.html')
-rw-r--r--html/projects/outline.html26
1 files changed, 0 insertions, 26 deletions
diff --git a/html/projects/outline.html b/html/projects/outline.html
deleted file mode 100644
index 67680b8f..00000000
--- a/html/projects/outline.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<h2>Integrating block-structured development and outline mode</h2>
-<p>
-Emacs already provides powerful outline facilities (cf. the
-outl-minor-mode setup for the well-known auc-tex package).
-Similarly, proof systems such as Isabelle/Isar are inherently based on
-block-structured proof texts, with compositional proof checking.
-</p><p>
-But Proof General currently offers a mostly linear model of
-incremental script management. The aim of this project is to extend that
-model to a hierarchic one: e.g. sub-proofs could be suppressed in the
-presentation, or even temporarily suspended (to achieve top-down
-development).
-</p><p>
-Outline support would be useful for the large scale structure of formal
-developments as well, e.g. support the basic arrangement into logical
-section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
-</p>
-<p>
-<b>Skills:</b>
-Some understanding of the workings of Emacs outline mode and Proof
-General script management. Good portion of Emacs lisp knowledge.
-</p><p>
-<b>Proposer:</b>
-<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
-</p>
-