| changeset 7947 | b999c1ab9327 |
| parent 7880 | 62fb24e28e5e |
| child 8041 | e3237d8c18d6 |
| 7946:95e1de322e82 | 7947:b999c1ab9327 |
|---|---|
37 drop_act i `` Restrict C `` (Acts F))" |
37 drop_act i `` Restrict C `` (Acts F))" |
38 |
38 |
39 (*simplifies the expression of specifications*) |
39 (*simplifies the expression of specifications*) |
40 constdefs |
40 constdefs |
41 sub :: ['a, 'a=>'b] => 'b |
41 sub :: ['a, 'a=>'b] => 'b |
42 "sub i f == f i" |
42 "sub == %i f. f i" |
43 |
43 |
44 |
44 |
45 end |
45 end |