# HG changeset patch
# User krauss
# Date 1273237437 -7200
# Node ID f5b63d2bd8fa056f02f6d9ba77740cdc581b828a
# Parent  ae397b810c8b160f72c6b8fa3241ec73b074415a
removed semicolons

diff -r ae397b810c8b -r f5b63d2bd8fa src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri May 07 15:03:53 2010 +0200
+++ b/src/HOL/Relation.thy	Fri May 07 15:03:57 2010 +0200
@@ -406,7 +406,7 @@
 lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
 by blast
 
-lemma fst_eq_Domain: "fst ` R = Domain R";
+lemma fst_eq_Domain: "fst ` R = Domain R"
 by (auto intro!:image_eqI)
 
 lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
@@ -457,7 +457,7 @@
 lemma Range_converse[simp]: "Range(r^-1) = Domain r"
 by blast
 
-lemma snd_eq_Range: "snd ` R = Range R";
+lemma snd_eq_Range: "snd ` R = Range R"
 by (auto intro!:image_eqI)