src/HOL/Integ/Equiv.ML
changeset 1978 e7df069acb74
parent 1894 c2c8279d40f0
child 2036 62ff902eeffc
equal deleted inserted replaced
1977:26edb2771d94 1978:e7df069acb74
     5     Copyright   1994 Universita' di Firenze
     5     Copyright   1994 Universita' di Firenze
     6     Copyright   1993  University of Cambridge
     6     Copyright   1993  University of Cambridge
     7 
     7 
     8 Equivalence relations in HOL Set Theory 
     8 Equivalence relations in HOL Set Theory 
     9 *)
     9 *)
       
    10 
       
    11 val RSLIST = curry (op MRS);
    10 
    12 
    11 open Equiv;
    13 open Equiv;
    12 
    14 
    13 Delrules [equalityI];
    15 Delrules [equalityI];
    14 
    16