Removed the unused rel_eq_cs
authorpaulson
Fri Jun 28 15:29:05 1996 +0200 (1996-06-28)
changeset 1842a9c36056d320
parent 1841 8e5e2fef6d26
child 1843 a6d7aef48c2f
Removed the unused rel_eq_cs
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Fri Jun 28 15:28:29 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Jun 28 15:29:05 1996 +0200
     1.3 @@ -181,10 +181,6 @@
     1.4                           addIs  [ImageI, DomainI, RangeI]
     1.5                           addSEs [ImageE, DomainE, RangeE];
     1.6  
     1.7 -AddSIs [equalityI];
     1.8 -
     1.9 -val rel_eq_cs = rel_cs addSIs [equalityI];
    1.10 -
    1.11  goal Relation.thy "R O id = R";
    1.12  by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
    1.13  qed "R_O_id";