105 |
105 |
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 transfer_method = Method.thms_ctxt_args (fn ths => fn ctxt => |
|
111 Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ctxt ths)); |
|
112 |
|
113 val setup = |
110 val setup = |
114 TransferData.init #> |
111 TransferData.init #> |
115 Attrib.add_attributes |
112 Attrib.add_attributes |
116 [("transfer_intro", Attrib.add_del_args intro_add intro_del, |
113 [("transfer_intro", Attrib.add_del_args intro_add intro_del, |
117 "declaration of transfer introduction rule"), |
114 "declaration of transfer introduction rule"), |
118 ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del, |
115 ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del, |
119 "declaration of transfer unfolding rule"), |
116 "declaration of transfer unfolding rule"), |
120 ("transfer_refold", Attrib.add_del_args refold_add refold_del, |
117 ("transfer_refold", Attrib.add_del_args refold_add refold_del, |
121 "declaration of transfer refolding rule")] #> |
118 "declaration of transfer refolding rule")] #> |
122 Method.add_method ("transfer", transfer_method, "transfer principle"); |
119 Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt => |
|
120 Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle"); |
123 |
121 |
124 end; |
122 end; |