src/HOL/IMP/Hoare.thy
changeset 2810 c4e16b36bc57
parent 1789 aade046ec6d5
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/IMP/Hoare.thy	Tue Mar 18 17:03:55 1997 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Mar 18 18:02:19 1997 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Inductive definition of Hoare logic
     1.5  *)
     1.6  
     1.7 -Hoare = Denotation +
     1.8 +Hoare = Denotation + Gfp +
     1.9  
    1.10  types assn = state => bool
    1.11  
    1.12 @@ -29,7 +29,7 @@
    1.13    conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.14            |- {P'}c{Q'}"
    1.15  
    1.16 -constdefs swp :: com => assn => assn
    1.17 -          "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    1.18 +constdefs wp :: com => assn => assn
    1.19 +          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    1.20  
    1.21  end