src/HOL/IMP/VC.thy
changeset 1481 03f096efa26d
parent 1476 608483c2122a
child 1696 e84bff5c519b
     1.1 --- a/src/HOL/IMP/VC.thy	Tue Feb 06 12:44:31 1996 +0100
     1.2 +++ b/src/HOL/IMP/VC.thy	Wed Feb 07 12:22:32 1996 +0100
     1.3 @@ -37,11 +37,11 @@
     1.4                                (I s & B b s --> wp c I s) & vc c I s)"
     1.5  
     1.6  primrec astrip acom
     1.7 -  astrip_Askip  "astrip Askip = skip"
     1.8 +  astrip_Askip  "astrip Askip = Skip"
     1.9    astrip_Aass   "astrip (Aass x a) = (x:=a)"
    1.10    astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    1.11 -  astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
    1.12 -  astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
    1.13 +  astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    1.14 +  astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    1.15  
    1.16  (* simultaneous computation of vc and wp: *)
    1.17  primrec vcwp acom