forget RPM;

--- a/Admin/polyml/polyml.spec	Fri Jan 19 11:53:21 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-Summary:	Poly/ML compiler and runtime system
-Name:		polyml
-Version:	3X
-Release:	2
-Group:		Development/Languages
-Copyright:	Cambridge University Technical Services Limited
-Url:		http://www.polyml.org
-Packager:	Markus Wenzel <[e-mail]>
-Prefix:		/usr/share
-
-%description
-Poly/ML is a full implementation of Standard ML available as
-open-source.
-
-It currently supports the ML 90 version of the language and a project
-is under way to bring this up to the ML 97 version.
-
-%install
-ln -sf /usr/share/polyml/bin/polyml /usr/bin/polyml
-
-%post
-ln -sf $RPM_INSTALL_PREFIX/polyml/bin/polyml /usr/bin/polyml
-
-%files
-/usr/share/polyml

--- a/Admin/proofgeneral/proofgeneral.spec	Fri Jan 19 11:53:21 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-Summary:	Proof General, Emacs interface for Proof Assistants
-Name:		proofgeneral
-Version:	3.2pre000923
-Release:	1
-Group:		Applications/Editors/Emacs
-Copyright:	LFCS, University of Edinburgh
-Url:		http://www.lfcs.informatics.ed.ac.uk/proofgen
-Packager:	Markus Wenzel <[e-mail]>
-Prefix:		/usr/share
-BuildArchitectures: noarch
-
-%description
-Proof General is a generic Emacs interface for proof assistants,
-suitable for use by pacifists and Emacs militants alike.
-It is supplied ready-customized for LEGO, Coq, and Isabelle.
-
-This distribution of Proof General is intended to be used together
-with Isabelle and Proof General.  It relies on Isabelle's automatic
-configuration of contributed packages.
-
-%prep
-find /usr/share/ProofGeneral/. -type f -print | xargs perl -pi -e 's:^#!.*/perl:#!usr/bin/perl:'
-
-%files
-%attr(-,root,root) /usr/share/ProofGeneral
-%attr(-,root,root) /usr/share/ProofGeneral-3.2pre000923

--- a/Admin/xsymbol/xsymbol.spec	Fri Jan 19 11:53:21 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-Summary:	X-Symbol mode for XEmacs to display mathematical symbols
-Name:		xsymbol
-Version:	3.3d
-Release:	1
-Group:		Applications/Editors/Emacs
-Copyright:	GPL
-Url:		http://www.fmi.uni-passau.de/~wedler/x-symbol/
-Packager:	Markus Wenzel <[e-mail]>
-Prefix:		/usr/share
-BuildArchitectures: noarch
-
-%description
-
-X-Symbol is an XEmacs package providing semi-WYSIWYG for LaTeX, HTML
-and other ``token languages''.  It uses additional fonts and provide
-input methods to insert their characters into your document.
-
-The main purpose of package X-Symbol is to provide some WYSIWYGness in
-an area where it greatly enhance the readability of your LaTeX or HTML
-source: using "real" characters for "tokens" like \oplus or &#8482;.
-It also provides input methods for these characters, both for the
-beginner and the expert (some users regard this as the main reason to
-use package X-Symbol). WYSIWYG super- and subscripts and
-images/figures are also supported.
-
-This distribution of X-Symbol is intended to be used together with
-Isabelle and Proof General.  It relies on Isabelle's automatic
-configuration of contributed packages.  Please ignore the installation
-instructions of X-Symbol!
-
-%prep
-find /usr/share/x-symbol -type f -print | xargs perl -pi -e 's:^#!.*/perl:#!usr/bin/perl:'
-
-%files
-%attr(-,root,root) /usr/share/x-symbol