Declare ML Module "demo_plugin".

Cmd1.
Cmd2 With Some Terminal Parameters.
Cmd3 42.
Cmd4 100 200 300 400.
Cmd5 Foo_5.
Cmd5 Bar_5.
Cmd6.
Cmd7.
Cmd7.
Cmd7.

Goal True.
Proof.
  tactic1.
  tactic2 Foo_2.
  tactic2 Bar_2.
Abort.