# HG changeset patch
# User nipkow
# Date 1369633330 -7200
# Node ID b8ea3e7a1b0701d30ae1489a0f7ed351a4a6be02
# Parent  32b1dbda331c2a286b0c91838e81e6150ff4faab
tuned

diff -r 32b1dbda331c -r b8ea3e7a1b07 src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Sun May 26 11:56:55 2013 +0200
+++ b/src/HOL/IMP/Hoare.thy	Mon May 27 07:42: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 32b1dbda331c -r b8ea3e7a1b07 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Sun May 26 11:56:55 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon May 27 07:42: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)