src/HOL/IMP/Hoare.thy
changeset 1476 608483c2122a
parent 1447 bc2c0acbbf29
child 1481 03f096efa26d
     1.1 --- a/src/HOL/IMP/Hoare.thy	Mon Feb 05 21:27:16 1996 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Mon Feb 05 21:29:06 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/IMP/Hoare.thy
     1.5 +(*  Title:      HOL/IMP/Hoare.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow
     1.8 +    Author:     Tobias Nipkow
     1.9      Copyright   1995 TUM
    1.10  
    1.11  Inductive definition of Hoare logic
    1.12 @@ -27,8 +27,8 @@
    1.13    hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    1.14                {{P}} ifc b then c else d {{Q}}"
    1.15    hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
    1.16 -	       {{P}} while b do c {{%s. P s & ~B b s}}"
    1.17 +               {{P}} while b do c {{%s. P s & ~B b s}}"
    1.18    hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    1.19 -		{{P'}}c{{Q'}}"
    1.20 +                {{P'}}c{{Q'}}"
    1.21  
    1.22  end