# HG changeset patch
# User paulson
# Date 842460367 -7200
# Node ID e7df069acb741c5f4ace028681cc4feb6531cb75
# Parent  26edb2771d94cc961f3cdc78bfdc002a1a4f7cd9
Moved RSLIST here from ../Relation.ML

diff -r 26edb2771d94 -r e7df069acb74 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Wed Sep 11 18:45:33 1996 +0200
+++ b/src/HOL/Integ/Equiv.ML	Wed Sep 11 18:46:07 1996 +0200
@@ -8,6 +8,8 @@
 Equivalence relations in HOL Set Theory 
 *)
 
+val RSLIST = curry (op MRS);
+
 open Equiv;
 
 Delrules [equalityI];