# HG changeset patch
# User paulson
# Date 888228940 -3600
# Node ID ecf8f17f6fe07bd992e464d782c9a88bd55e5fb5
# Parent  1b40fcac5a093020b86424064939b7126e19b228
New laws for id

diff -r 1b40fcac5a09 -r ecf8f17f6fe0 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Sun Feb 22 14:12:23 1998 +0100
+++ b/src/HOL/Relation.ML	Mon Feb 23 11:15:40 1998 +0100
@@ -112,6 +112,11 @@
 by (Blast_tac 1);
 qed "inverse_comp";
 
+goal Relation.thy "id^-1 = id";
+by (Blast_tac 1);
+qed "inverse_id";
+Addsimps [inverse_id];
+
 (** Domain **)
 
 qed_goalw "Domain_iff" Relation.thy [Domain_def]
@@ -130,6 +135,11 @@
 AddIs  [DomainI];
 AddSEs [DomainE];
 
+goal thy "Domain id = UNIV";
+by (Blast_tac 1);
+qed "Domain_id";
+Addsimps [Domain_id];
+
 (** Range **)
 
 qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
@@ -145,6 +155,11 @@
 AddIs  [RangeI];
 AddSEs [RangeE];
 
+goal thy "Range id = UNIV";
+by (Blast_tac 1);
+qed "Range_id";
+Addsimps [Range_id];
+
 (*** Image of a set under a relation ***)
 
 qed_goalw "Image_iff" Relation.thy [Image_def]