# HG changeset patch
# User nipkow
# Date 830599651 -7200
# Node ID 3452958f85a8d8c9dd97411fcabe9fc4141b000b
# Parent  7083f6b054231dd531b087e75e3c280b596a0b90
Added R_O_id and id_O_R

diff -r 7083f6b05423 -r 3452958f85a8 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Sat Apr 27 12:05:58 1996 +0200
+++ b/src/HOL/Relation.ML	Sat Apr 27 12:07:31 1996 +0200
@@ -29,6 +29,7 @@
 goalw Relation.thy [id_def] "(a,b):id = (a=b)";
 by (fast_tac prod_cs 1);
 qed "pair_in_id_conv";
+Addsimps [pair_in_id_conv];
 
 
 (** Composition of two relations **)
@@ -172,4 +173,12 @@
 
 val rel_eq_cs = rel_cs addSIs [equalityI];
 
-Addsimps [pair_in_id_conv];
+goal Relation.thy "R O id = R";
+by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
+qed "R_O_id";
+
+goal Relation.thy "id O R = R";
+by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
+qed "id_O_R";
+
+Addsimps [R_O_id,id_O_R];