# HG changeset patch
# User paulson
# Date 835968545 -7200
# Node ID a9c36056d320ae1be67d6fe8f3abead06f677394
# Parent  8e5e2fef6d269378389faa982f7fc2f4a9ab3867
Removed the unused rel_eq_cs

diff -r 8e5e2fef6d26 -r a9c36056d320 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Jun 28 15:28:29 1996 +0200
+++ b/src/HOL/Relation.ML	Fri Jun 28 15:29:05 1996 +0200
@@ -181,10 +181,6 @@
                          addIs  [ImageI, DomainI, RangeI]
                          addSEs [ImageE, DomainE, RangeE];
 
-AddSIs [equalityI];
-
-val rel_eq_cs = rel_cs addSIs [equalityI];
-
 goal Relation.thy "R O id = R";
 by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
 qed "R_O_id";