];
level3_term: [
[ u = URI -> N.UriPattern (UriManager.uri_of_string u)
+ | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
| IMPLICIT -> N.ImplicitPattern
| id = IDENT -> N.VarPattern id
| LPAREN; terms = LIST1 SELF; RPAREN ->
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body))
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ body = term ->
+ G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.Obj (loc, N.Theorem (flavour, name, typ, body))