src/HOL/Integ/Equiv.ML
changeset 1978 e7df069acb74
parent 1894 c2c8279d40f0
child 2036 62ff902eeffc
     1.1 --- a/src/HOL/Integ/Equiv.ML	Wed Sep 11 18:45:33 1996 +0200
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Wed Sep 11 18:46:07 1996 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  Equivalence relations in HOL Set Theory 
     1.5  *)
     1.6  
     1.7 +val RSLIST = curry (op MRS);
     1.8 +
     1.9  open Equiv;
    1.10  
    1.11  Delrules [equalityI];