[m-rev.] diff: delete unused library files

[Julien Fischer]

library/bintree.m:
library/bintree_set.m:
library/graph.m:
library/group.m:
library/relation.m:
library/svrelation.m:
	Delete these files: they are no longer needed.
	(Previously, when using CVS we didn't delete them
	in case we needed to reuse them, but that no longer
	applies.

Julien.

diff --git a/library/bintree.m b/library/bintree.m
deleted file mode 100644
index 6cf0bd2..0000000
--- a/library/bintree.m
+++ /dev/null
@@ -1,3 +0,0 @@
-%---------------------------------------------------------------------------%
-% THIS FILE IS NO LONGER USED.
-%---------------------------------------------------------------------------%
diff --git a/library/bintree_set.m b/library/bintree_set.m
deleted file mode 100644
index 6cf0bd2..0000000
--- a/library/bintree_set.m
+++ /dev/null
@@ -1,3 +0,0 @@
-%---------------------------------------------------------------------------%
-% THIS FILE IS NO LONGER USED.
-%---------------------------------------------------------------------------%
diff --git a/library/graph.m b/library/graph.m
deleted file mode 100644
index 6cf0bd2..0000000
--- a/library/graph.m
+++ /dev/null
@@ -1,3 +0,0 @@
-%---------------------------------------------------------------------------%
-% THIS FILE IS NO LONGER USED.
-%---------------------------------------------------------------------------%
diff --git a/library/group.m b/library/group.m
deleted file mode 100644
index 6cf0bd2..0000000
--- a/library/group.m
+++ /dev/null
@@ -1,3 +0,0 @@
-%---------------------------------------------------------------------------%
-% THIS FILE IS NO LONGER USED.
-%---------------------------------------------------------------------------%
diff --git a/library/relation.m b/library/relation.m
deleted file mode 100644
index 6cf0bd2..0000000
--- a/library/relation.m
+++ /dev/null
@@ -1,3 +0,0 @@
-%---------------------------------------------------------------------------%
-% THIS FILE IS NO LONGER USED.
-%---------------------------------------------------------------------------%
diff --git a/library/svrelation.m b/library/svrelation.m
deleted file mode 100644
index 6cf0bd2..0000000
--- a/library/svrelation.m
+++ /dev/null
@@ -1,3 +0,0 @@
-%---------------------------------------------------------------------------%
-% THIS FILE IS NO LONGER USED.
-%---------------------------------------------------------------------------%