34 val internal_source: Token.src parser |
34 val internal_source: Token.src parser |
35 val internal_name: Token.name_value parser |
35 val internal_name: Token.name_value parser |
36 val internal_typ: typ parser |
36 val internal_typ: typ parser |
37 val internal_term: term parser |
37 val internal_term: term parser |
38 val internal_fact: thm list parser |
38 val internal_fact: thm list parser |
39 val internal_attribute: (morphism -> attribute) parser |
39 val internal_attribute: attribute Morphism.entity parser |
40 val internal_declaration: declaration parser |
40 val internal_declaration: Morphism.declaration parser |
41 val named_source: (Token.T -> Token.src) -> Token.src parser |
41 val named_source: (Token.T -> Token.src) -> Token.src parser |
42 val named_typ: (string -> typ) -> typ parser |
42 val named_typ: (string -> typ) -> typ parser |
43 val named_term: (string -> term) -> term parser |
43 val named_term: (string -> term) -> term parser |
44 val named_fact: (string -> string option * thm list) -> thm list parser |
44 val named_fact: (string -> string option * thm list) -> thm list parser |
45 val named_attribute: (string * Position.T -> morphism -> attribute) -> |
45 val named_attribute: (string * Position.T -> attribute Morphism.entity) -> |
46 (morphism -> attribute) parser |
46 attribute Morphism.entity parser |
47 val embedded_declaration: (Input.source -> declaration) -> declaration parser |
47 val embedded_declaration: (Input.source -> Morphism.declaration) -> Morphism.declaration parser |
48 val typ_abbrev: typ context_parser |
48 val typ_abbrev: typ context_parser |
49 val typ: typ context_parser |
49 val typ: typ context_parser |
50 val term: term context_parser |
50 val term: term context_parser |
51 val term_pattern: term context_parser |
51 val term_pattern: term context_parser |
52 val term_abbrev: term context_parser |
52 val term_abbrev: term context_parser |