author | paulson |
Fri, 28 Jun 1996 15:29:05 +0200 | |
changeset 1842 | a9c36056d320 |
parent 1841 | 8e5e2fef6d26 |
child 1843 | a6d7aef48c2f |
--- 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";