- val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
- val focus : output_status -> ProofEngineTypes.goal -> input_status
- end
+ val get_stack : input_status -> stack
+ val set_stack : stack -> output_status -> output_status
+
+ val inject : input_status -> output_status
+ val focus : goal -> output_status -> input_status
+ end *)