106 fun add_const c = Context.theory_map (TransferData.map |
106 fun add_const c = Context.theory_map (TransferData.map |
107 (fn {intros,unfolds,refolds,consts} => |
107 (fn {intros,unfolds,refolds,consts} => |
108 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) |
108 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) |
109 |
109 |
110 val setup = |
110 val setup = |
111 Attrib.add_attributes |
111 Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del) |
112 [("transfer_intro", Attrib.add_del_args intro_add intro_del, |
112 "declaration of transfer introduction rule" #> |
113 "declaration of transfer introduction rule"), |
113 Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del) |
114 ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del, |
114 "declaration of transfer unfolding rule" #> |
115 "declaration of transfer unfolding rule"), |
115 Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del) |
116 ("transfer_refold", Attrib.add_del_args refold_add refold_del, |
116 "declaration of transfer refolding rule" #> |
117 "declaration of transfer refolding rule")] #> |
117 Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt => |
118 Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt => |
118 SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle"; |
119 SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle"); |
|
120 |
119 |
121 end; |
120 end; |