--- 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)"
--- 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