changeset 1296 | ae31bb7774a7 |
parent 121 | d392174734e9 |
child 1361 | 90d615b599d9 |
1295:27c1e88a62b4 | 1296:ae31bb7774a7 |
---|---|
76 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] |
76 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] |
77 end; |
77 end; |
78 end; |
78 end; |
79 structure S43_Prover = Modal_ProverFun(MP_Rule); |
79 structure S43_Prover = Modal_ProverFun(MP_Rule); |
80 |
80 |
81 make_chart (); (*make HTML chart*) |
|
82 |
|
81 val Modal_build_completed = (); (*indicate successful build*) |
83 val Modal_build_completed = (); (*indicate successful build*) |
82 |
84 |
83 (*printing functions are inherited from LK*) |
85 (*printing functions are inherited from LK*) |