16 val defined: theory -> string -> bool |
16 val defined: theory -> string -> bool |
17 val attribute: theory -> src -> attribute |
17 val attribute: theory -> src -> attribute |
18 val attribute_i: theory -> src -> attribute |
18 val attribute_i: theory -> src -> attribute |
19 val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list |
19 val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list |
20 val map_specs: ('a -> 'att) -> |
20 val map_specs: ('a -> 'att) -> |
21 (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list |
21 (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list |
22 val map_facts: ('a -> 'att) -> |
22 val map_facts: ('a -> 'att) -> |
23 (('c * 'a list) * ('d * 'a list) list) list -> |
23 (('c * 'a list) * ('d * 'a list) list) list -> |
24 (('c * 'att list) * ('d * 'att list) list) list |
24 (('c * 'att list) * ('d * 'att list) list) list |
|
25 val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) -> |
|
26 (('c * 'a list) * ('b * 'a list) list) list -> |
|
27 (('c * 'att list) * ('fact * 'att list) list) list |
25 val crude_closure: Proof.context -> src -> src |
28 val crude_closure: Proof.context -> src -> src |
26 val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory |
29 val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory |
27 val syntax: attribute context_parser -> src -> attribute |
30 val syntax: attribute context_parser -> src -> attribute |
28 val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory |
31 val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory |
29 val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> |
32 val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> |
118 end; |
121 end; |
119 in attr end; |
122 in attr end; |
120 |
123 |
121 fun attribute thy = attribute_i thy o intern_src thy; |
124 fun attribute thy = attribute_i thy o intern_src thy; |
122 |
125 |
123 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK |
126 fun eval_thms ctxt args = ProofContext.note_thmss_i Thm.theoremK |
124 [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt |
127 [(Thm.empty_binding, args |> map (fn (a, atts) => |
|
128 (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt |
125 |> fst |> maps snd; |
129 |> fst |> maps snd; |
126 |
130 |
127 |
131 |
128 (* attributed declarations *) |
132 (* attributed declarations *) |
129 |
133 |
130 fun map_specs f = map (apfst (apsnd (map f))); |
134 fun map_specs f = map (apfst (apsnd (map f))); |
|
135 |
131 fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f)))); |
136 fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f)))); |
|
137 fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g))); |
132 |
138 |
133 |
139 |
134 (* crude_closure *) |
140 (* crude_closure *) |
135 |
141 |
136 (*Produce closure without knowing facts in advance! The following |
142 (*Produce closure without knowing facts in advance! The following |