130 | rule2stac thy (Rule.Eval (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string |
130 | rule2stac thy (Rule.Eval (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string |
131 (get_calc_prog_id (Proof_Context.init_global thy) c))) |
131 (get_calc_prog_id (Proof_Context.init_global thy) c))) |
132 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string |
132 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string |
133 (get_calc_prog_id (Proof_Context.init_global thy) c))) |
133 (get_calc_prog_id (Proof_Context.init_global thy) c))) |
134 | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls)) |
134 | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls)) |
135 | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string r ^ "\""); |
135 | rule2stac thy r = raise ERROR ("rule2stac: not applicable to \"" ^ |
|
136 Rule.to_string (Proof_Context.init_global thy) r ^ "\""); |
136 fun rule2stac_inst _ (Rule.Thm (thmID, _)) = |
137 fun rule2stac_inst _ (Rule.Thm (thmID, _)) = |
137 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID)) |
138 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID)) |
138 | rule2stac_inst thy (Rule.Eval (c, _)) = |
139 | rule2stac_inst thy (Rule.Eval (c, _)) = |
139 Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c))) |
140 Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c))) |
140 | rule2stac_inst thy (Rule.Cal1 (c, _)) = |
141 | rule2stac_inst thy (Rule.Cal1 (c, _)) = |
141 Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c))) |
142 Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c))) |
142 | rule2stac_inst _ (Rule.Rls_ rls) = |
143 | rule2stac_inst _ (Rule.Rls_ rls) = |
143 Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls)) |
144 Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls)) |
144 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string r ^ "\""); |
145 | rule2stac_inst thy r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ |
|
146 Rule.to_string (Proof_Context.init_global thy) r ^ "\""); |
145 |
147 |
146 (*for appropriate nesting take stacs in _reverse_ order*) |
148 (*for appropriate nesting take stacs in _reverse_ order*) |
147 fun op #>@ sts [s] = SEq $ s $ sts |
149 fun op #>@ sts [s] = SEq $ s $ sts |
148 | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss |
150 | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss |
149 | op #>@ t ts = |
151 | op #>@ t ts = |