From c9e9c691c353d5d4835551de8d7d1f4c0ec74b9f Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 24 May 2017 11:14:51 -0400 Subject: Remove mmm and ML4PG contribs and remove references to them in code and docs --- doc/ProofGeneral.texi | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'doc') 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. -- cgit v1.2.3