1.1 --- a/src/HOL/IMP/Hoare.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -10,8 +10,9 @@
     1.4  
     1.5  types assn = "state => bool"
     1.6  
     1.7 -constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
     1.8 -          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
     1.9 +definition
    1.10 +  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    1.11 +  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
    1.12  
    1.13  inductive
    1.14    hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    1.15 @@ -26,8 +27,9 @@
    1.16  | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.17            |- {P'}c{Q'}"
    1.18  
    1.19 -constdefs wp :: "com => assn => assn"
    1.20 -          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    1.21 +definition
    1.22 +  wp :: "com => assn => assn" where
    1.23 +  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
    1.24  
    1.25  (*
    1.26  Soundness (and part of) relative completeness of Hoare rules