equal
deleted
inserted
replaced
33 "meta predicate" basevars, which is defined here. |
33 "meta predicate" basevars, which is defined here. |
34 *) |
34 *) |
35 stvars :: "'a stfun => bool" |
35 stvars :: "'a stfun => bool" |
36 |
36 |
37 syntax |
37 syntax |
38 "PRED" :: "lift => 'a" ("PRED _") |
38 "_PRED" :: "lift => 'a" ("PRED _") |
39 "_stvars" :: "lift => bool" ("basevars _") |
39 "_stvars" :: "lift => bool" ("basevars _") |
40 |
40 |
41 translations |
41 translations |
42 "PRED P" => "(P::state => _)" |
42 "PRED P" => "(P::state => _)" |
43 "_stvars" == "CONST stvars" |
43 "_stvars" == "CONST stvars" |