src/Pure/Thy/thy_header.ML
changeset 59735 24bee1b11fce
parent 59694 d2bb4b5ed862
child 59934 b65c4370f831
equal deleted inserted replaced
59729:ba54b27d733d 59735:24bee1b11fce
    10   type header =
    10   type header =
    11    {name: string * Position.T,
    11    {name: string * Position.T,
    12     imports: (string * Position.T) list,
    12     imports: (string * Position.T) list,
    13     keywords: keywords}
    13     keywords: keywords}
    14   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
    14   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
       
    15   val theoryN: string
    15   val bootstrap_keywords: Keyword.keywords
    16   val bootstrap_keywords: Keyword.keywords
    16   val add_keywords: keywords -> theory -> theory
    17   val add_keywords: keywords -> theory -> theory
    17   val get_keywords: theory -> Keyword.keywords
    18   val get_keywords: theory -> Keyword.keywords
    18   val get_keywords': Proof.context -> Keyword.keywords
    19   val get_keywords': Proof.context -> Keyword.keywords
    19   val args: header parser
    20   val args: header parser