src/HOL/Relation.ML
changeset 10786 04ee73606993
parent 9969 4753185f1dd2
child 10797 028d22926a41
     1.1 --- a/src/HOL/Relation.ML	Fri Jan 05 10:18:46 2001 +0100
     1.2 +++ b/src/HOL/Relation.ML	Fri Jan 05 10:19:14 2001 +0100
     1.3 @@ -233,6 +233,15 @@
     1.4  AddIs  [DomainI];
     1.5  AddSEs [DomainE];
     1.6  
     1.7 +Goal "Domain {} = {}";
     1.8 +by (Blast_tac 1); 
     1.9 +qed "Domain_empty";
    1.10 +Addsimps [Domain_empty];
    1.11 +
    1.12 +Goal "Domain (insert (a, b) r) = insert a (Domain r)";
    1.13 +by (Blast_tac 1); 
    1.14 +qed "Domain_insert";
    1.15 +
    1.16  Goal "Domain Id = UNIV";
    1.17  by (Blast_tac 1);
    1.18  qed "Domain_Id";
    1.19 @@ -284,6 +293,15 @@
    1.20  AddIs  [RangeI];
    1.21  AddSEs [RangeE];
    1.22  
    1.23 +Goal "Range {} = {}";
    1.24 +by (Blast_tac 1); 
    1.25 +qed "Range_empty";
    1.26 +Addsimps [Range_empty];
    1.27 +
    1.28 +Goal "Range (insert (a, b) r) = insert b (Range r)";
    1.29 +by (Blast_tac 1); 
    1.30 +qed "Range_insert";
    1.31 +
    1.32  Goal "Range Id = UNIV";
    1.33  by (Blast_tac 1);
    1.34  qed "Range_Id";
    1.35 @@ -350,7 +368,6 @@
    1.36  by (Blast_tac 1);
    1.37  qed "rev_ImageI";
    1.38  
    1.39 -
    1.40  Goal "R^^{} = {}";
    1.41  by (Blast_tac 1);
    1.42  qed "Image_empty";