--- 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]