--- a/src/HOL/Relation.ML Fri Jan 05 10:18:46 2001 +0100
+++ b/src/HOL/Relation.ML Fri Jan 05 10:19:14 2001 +0100
@@ -233,6 +233,15 @@
AddIs [DomainI];
AddSEs [DomainE];
+Goal "Domain {} = {}";
+by (Blast_tac 1);
+qed "Domain_empty";
+Addsimps [Domain_empty];
+
+Goal "Domain (insert (a, b) r) = insert a (Domain r)";
+by (Blast_tac 1);
+qed "Domain_insert";
+
Goal "Domain Id = UNIV";
by (Blast_tac 1);
qed "Domain_Id";
@@ -284,6 +293,15 @@
AddIs [RangeI];
AddSEs [RangeE];
+Goal "Range {} = {}";
+by (Blast_tac 1);
+qed "Range_empty";
+Addsimps [Range_empty];
+
+Goal "Range (insert (a, b) r) = insert b (Range r)";
+by (Blast_tac 1);
+qed "Range_insert";
+
Goal "Range Id = UNIV";
by (Blast_tac 1);
qed "Range_Id";
@@ -350,7 +368,6 @@
by (Blast_tac 1);
qed "rev_ImageI";
-
Goal "R^^{} = {}";
by (Blast_tac 1);
qed "Image_empty";