Moved RSLIST here from ../Relation.ML
authorpaulson
Wed Sep 11 18:46:07 1996 +0200 (1996-09-11)
changeset 1978e7df069acb74
parent 1977 26edb2771d94
child 1979 91c74763c5a3
Moved RSLIST here from ../Relation.ML
src/HOL/Integ/Equiv.ML
     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];