da,ds:Decl, init:({ds}
Prop), trans:({ds}(
da){ds}Prop). mk_sm(da, ds, init, trans) 
sm{i:l}()| Who Cites mk sm? | |
| mk_sm | Def mk_sm(da, ds, init, trans) == < da,ds,init,trans > |
| Thm* da,ds:Decl, init:({ds}Prop), trans:({ds}(da){ds}Prop). mk_sm(da, ds, init, trans) sm{i:l}() |
| Syntax: | mk_sm(da, ds, init, trans) | has structure: | mk_sm(da; ds; init; trans) |
About:
 |  |  |  |  |  |