src/Pure/Isar/attrib.ML
changeset 57936 74ea9ba645c3
parent 57927 f14c1248d064
child 57937 3bc4725b313e
equal deleted inserted replaced
57935:c578f3a37a67 57936:74ea9ba645c3
    36   val local_notes: string -> (binding * (thm list * src list) list) list ->
    36   val local_notes: string -> (binding * (thm list * src list) list) list ->
    37     Proof.context -> (string * thm list) list * Proof.context
    37     Proof.context -> (string * thm list) list * Proof.context
    38   val generic_notes: string -> (binding * (thm list * src list) list) list ->
    38   val generic_notes: string -> (binding * (thm list * src list) list) list ->
    39     Context.generic -> (string * thm list) list * Context.generic
    39     Context.generic -> (string * thm list) list * Context.generic
    40   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    40   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
       
    41   val attribute_syntax: attribute context_parser -> Args.src -> attribute
    41   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    42   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    42   val local_setup: Binding.binding -> attribute context_parser -> string ->
    43   val local_setup: Binding.binding -> attribute context_parser -> string ->
    43     local_theory -> local_theory
    44     local_theory -> local_theory
    44   val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    45   val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    45   val internal: (morphism -> attribute) -> src
    46   val internal: (morphism -> attribute) -> src