| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))