135 open Hints_declaration
164 Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
165 SmallstepExec.trans_system
168 Joint_semantics.sem_params -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
170 val joint_preclassified_system :
171 Joint_semantics.sem_params -> Measurable.preclassified_system