From b37bf74fc2d6309a5ae3dc6b55e8488409976775 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 Feb 2000 06:19:39 +0000
Subject: New projects directory.

---
 html/projects/outline.html | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 html/projects/outline.html

(limited to 'html/projects/outline.html')

diff --git a/html/projects/outline.html b/html/projects/outline.html
new file mode 100644
index 00000000..67680b8f
--- /dev/null
+++ b/html/projects/outline.html
@@ -0,0 +1,26 @@
+<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>
+
-- 
cgit v1.2.3