removed semicolons
authorkrauss
Fri May 07 15:03:57 2010 +0200 (2010-05-07)
changeset 36729f5b63d2bd8fa
parent 36728 ae397b810c8b
child 36730 bca8762be737
removed semicolons
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Fri May 07 15:03:53 2010 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri May 07 15:03:57 2010 +0200
     1.3 @@ -406,7 +406,7 @@
     1.4  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
     1.5  by blast
     1.6  
     1.7 -lemma fst_eq_Domain: "fst ` R = Domain R";
     1.8 +lemma fst_eq_Domain: "fst ` R = Domain R"
     1.9  by (auto intro!:image_eqI)
    1.10  
    1.11  lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    1.12 @@ -457,7 +457,7 @@
    1.13  lemma Range_converse[simp]: "Range(r^-1) = Domain r"
    1.14  by blast
    1.15  
    1.16 -lemma snd_eq_Range: "snd ` R = Range R";
    1.17 +lemma snd_eq_Range: "snd ` R = Range R"
    1.18  by (auto intro!:image_eqI)
    1.19  
    1.20