diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-05-24 11:14:51 -0400 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-05-24 11:14:51 -0400 |
| commit | c9e9c691c353d5d4835551de8d7d1f4c0ec74b9f (patch) | |
| tree | f89d20d989b309730281d4266b734e0adaed1867 /doc | |
| parent | afb29a670c537412d09cec703da7e8821c658196 (diff) | |
Remove mmm and ML4PG contribs and remove references to them in code and docs
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 79694197..945e6821 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4,7 +4,7 @@ @c @c @c TODO: -@c MMM support, Theorem dependencies, history in script and response, +@c Theorem dependencies, history in script and response, @c identifier info commands @@ -5455,7 +5455,7 @@ URL of web page for Isabelle. -@c FIXME todo: theorem dependencies, MMM +@c FIXME todo: theorem dependencies @c ================================================================= @@ -6144,9 +6144,8 @@ Summer Schools. Many new features have been added to enhance Coq mode Support has been added for the useful Emacs packages Speedbar @c @uref{http://cedet.sourceforge.net/speedbar.shtml,Speedbar} -and Index Menu, both usually distributed with Emacs. Compatible -versions of the Emacs packages Math-Menu (for Unicode symbols) and MMM -Mode (for multiple modes in one buffer) are bundled with Proof General. +and Index Menu, both usually distributed with Emacs. A compatible +version of the Emacs package Math-Menu (for Unicode symbols) is bundled with Proof General. An experimental Unicode Tokens package has been added which will replace X-Symbol. |