# HG changeset patch
# User nipkow
# Date 1369633450 -7200
# Node ID 3c22e72603b3934db0fcbb274214c56ce63eb622
# Parent  3c18725d576af76358c40446034ea7f976d1fd8e# Parent  b8ea3e7a1b0701d30ae1489a0f7ed351a4a6be02
merged

diff -r 3c18725d576a -r 3c22e72603b3 src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Sun May 26 22:57:48 2013 +0200
+++ b/src/HOL/IMP/Hoare.thy	Mon May 27 07:44:10 2013 +0200
@@ -8,6 +8,10 @@
 
 type_synonym assn = "state \<Rightarrow> bool"
 
+definition
+hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
+"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
+
 abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
   ("_[_'/_]" [1000,0,0] 999)
 where "s[a/x] == s(x := aval a s)"
diff -r 3c18725d576a -r 3c22e72603b3 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Sun May 26 22:57:48 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon May 27 07:44:10 2013 +0200
@@ -4,10 +4,6 @@
 
 subsection "Soundness"
 
-definition
-hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
-"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
-
 lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
 proof(induction rule: hoare.induct)
   case (While P b c)