--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon Mar 01 13:40:23 2010 +0100
@@ -42,7 +42,7 @@
"Sem(While b x c) s s' =
(if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
-constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
"Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"