71 type binding = binding * attribute list |
71 type binding = binding * attribute list |
72 val empty_binding: binding |
72 val empty_binding: binding |
73 val rule_attribute: (Context.generic -> thm -> thm) -> attribute |
73 val rule_attribute: (Context.generic -> thm -> thm) -> attribute |
74 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
74 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
75 val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute |
75 val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute |
76 val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm |
76 val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic |
77 val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic |
77 val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic |
78 val theory_attributes: attribute list -> theory * thm -> theory * thm |
78 val theory_attributes: attribute list -> thm -> theory -> thm * theory |
79 val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm |
79 val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context |
80 val no_attributes: 'a -> 'a * 'b list |
80 val no_attributes: 'a -> 'a * 'b list |
81 val simple_fact: 'a -> ('a * 'b list) list |
81 val simple_fact: 'a -> ('a * 'b list) list |
82 val tag_rule: Properties.entry -> thm -> thm |
82 val tag_rule: Properties.entry -> thm -> thm |
83 val untag_rule: string -> thm -> thm |
83 val untag_rule: string -> thm -> thm |
84 val tag: Properties.entry -> attribute |
84 val tag: Properties.entry -> attribute |
401 |
401 |
402 fun rule_attribute f (x, th) = (NONE, SOME (f x th)); |
402 fun rule_attribute f (x, th) = (NONE, SOME (f x th)); |
403 fun declaration_attribute f (x, th) = (SOME (f th x), NONE); |
403 fun declaration_attribute f (x, th) = (SOME (f th x), NONE); |
404 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; |
404 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; |
405 |
405 |
406 fun apply_attribute (att: attribute) (x, th) = |
406 fun apply_attribute (att: attribute) th x = |
407 let val (x', th') = att (x, th) |
407 let val (x', th') = att (x, th) |
408 in (the_default x x', the_default th th') end; |
408 in (the_default th th', the_default x x') end; |
409 |
409 |
410 fun attribute_declaration att th x = #1 (apply_attribute att (x, th)); |
410 fun attribute_declaration att th x = #2 (apply_attribute att th x); |
411 |
411 |
412 fun apply_attributes mk dest = |
412 fun apply_attributes mk dest = |
413 let |
413 let |
414 fun app [] = I |
414 fun app [] th x = (th, x) |
415 | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts; |
415 | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; |
416 in app end; |
416 in app end; |
417 |
417 |
418 val theory_attributes = apply_attributes Context.Theory Context.the_theory; |
418 val theory_attributes = apply_attributes Context.Theory Context.the_theory; |
419 val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
419 val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
420 |
420 |