(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)