| changeset 1978 | e7df069acb74 |
| parent 1894 | c2c8279d40f0 |
| child 2036 | 62ff902eeffc |
| 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 |