aboutsummaryrefslogtreecommitdiff
path: root/doc/PG-adapting.texi
diff options
context:
space:
mode:
authorDavid Aspinall2000-09-13 15:02:36 +0000
committerDavid Aspinall2000-09-13 15:02:36 +0000
commit7e254b5eba8ef2eb6d91ee8354a064a06037998c (patch)
tree61014d7939a4231f6167a44a37612fe831f91c19 /doc/PG-adapting.texi
parent7139ed1fbdcab00bb678e4a9897f3d80bd087098 (diff)
Minor improvements
Diffstat (limited to 'doc/PG-adapting.texi')
-rw-r--r--doc/PG-adapting.texi10
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 2661aeee..bb7daf39 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -200,15 +200,15 @@ grown more flexible and useful as it has been adapted to more proof
assistants. Typically, adding support for a new prover improves support
for others, both because the code becomes more robust, and because new
ideas are brought into the generic setting. You should understand that
-the Proof General framework has been built as a product line
-architecture: generality has been introduced piecemeal in a
+the Proof General framework has been built as a "product line
+architecture": generality has been introduced step-by-step in a
demand-driven way, rather than at the outset as a grand design.
(Despite this strategy, the interface has a surprisingly clean
-structure). This approach means that we fully expect hiccups when
+structure). The approach means that we fully expect hiccups when
adding support for new assistants, so the generic core may need
extension or modification. To support this we have an open development
-style: if you require changes in the generic support, please contact us,
-or make adjustments yourself and send them to us.
+method: if you require changes in the generic support, please contact us
+(or make adjustments yourself and send them to us).
Proof General has a home page at
@uref{http://www.lfcs.informatics.ed.ac.uk/proofgen}. Visit this page