--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/polyml.spec Mon Sep 11 20:44:53 2000 +0200
@@ -0,0 +1,25 @@
+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 <wenzelm@in.tum.de>
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/proofgeneral/proofgeneral.spec Mon Sep 11 20:44:53 2000 +0200
@@ -0,0 +1,23 @@
+Summary: Proof General, Emacs interface for Proof Assistants
+Name: proofgeneral
+Version: 3.2pre
+Release: 1
+Group: Applications/Editors/Emacs
+Copyright: LFCS, University of Edinburgh
+Url: http://www.lfcs.informatics.ed.ac.uk/proofgen
+Packager: Markus Wenzel <wenzelm@in.tum.de>
+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.
+
+%files
+%attr(-,root,root) /usr/share/ProofGeneral