# HG changeset patch
# User nipkow
# Date 1371629184 -7200
# Node ID ee996ca08de3f7e1bbdd7637ed289cbbfc72a231
# Parent  e65dedce4a1757cd74e727cca5ad79d9c7dc31a1
added lemma

diff -r e65dedce4a17 -r ee996ca08de3 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue Jun 18 15:52:47 2013 -0700
+++ b/src/HOL/IMP/Denotation.thy	Wed Jun 19 10:06:24 2013 +0200
@@ -121,12 +121,9 @@
 lemma cont_W: "cont(W b r)"
 by(auto simp: cont_def W_def)
 
+
 subsection{*The denotational semantics is deterministic*}
 
-(* FIXME mv *)
-lemma simgle_valued_empty[simp]: "single_valued {}"
-by(simp add: single_valued_def)
-
 lemma single_valued_UN_chain:
   assumes "chain S" "(\<And>n. single_valued (S n))"
   shows "single_valued(UN n. S n)"
diff -r e65dedce4a17 -r ee996ca08de3 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Jun 18 15:52:47 2013 -0700
+++ b/src/HOL/Relation.thy	Wed Jun 19 10:06:24 2013 +0200
@@ -416,6 +416,9 @@
   "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   by (simp add: single_valued_def)
 
+lemma simgle_valued_empty[simp]: "single_valued {}"
+by(simp add: single_valued_def)
+
 lemma single_valued_subset:
   "r \<subseteq> s ==> single_valued s ==> single_valued r"
   by (unfold single_valued_def) blast