src/HOL/IMP/VC.thy
 changeset 3842 b55686a7b22c parent 2810 c4e16b36bc57 child 4897 be11be0b6ea1
```     1.1 --- a/src/HOL/IMP/VC.thy	Fri Oct 10 18:37:49 1997 +0200
1.2 +++ b/src/HOL/IMP/VC.thy	Fri Oct 10 19:02:28 1997 +0200
1.3 @@ -23,14 +23,14 @@
1.4
1.5  primrec awp acom
1.6    "awp Askip Q = Q"
1.7 -  "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
1.8 +  "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
1.9    "awp (Asemi c d) Q = awp c (awp d Q)"
1.10    "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
1.11    "awp (Awhile b I c) Q = I"
1.12
1.13  primrec vc acom
1.14 -  "vc Askip Q = (%s.True)"
1.15 -  "vc (Aass x a) Q = (%s.True)"
1.16 +  "vc Askip Q = (%s. True)"
1.17 +  "vc (Aass x a) Q = (%s. True)"
1.18    "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
1.19    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)"
1.20    "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
1.21 @@ -45,8 +45,8 @@
1.22
1.23  (* simultaneous computation of vc and awp: *)
1.24  primrec vcawp acom
1.25 -  "vcawp Askip Q = (%s.True, Q)"
1.26 -  "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
1.27 +  "vcawp Askip Q = (%s. True, Q)"
1.28 +  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
1.29    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
1.30                                (vcc,wpc) = vcawp c wpd
1.31                            in (%s. vcc s & vcd s, wpc))"
```