changeset 52392 | ee996ca08de3 |
parent 52389 | 3971dd9ca831 |
--- 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)"