equal
deleted
inserted
replaced
258 Rewrite_Inst (Subst.T_to_input ctxt subst, thm'') |
258 Rewrite_Inst (Subst.T_to_input ctxt subst, thm'') |
259 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) |
259 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) |
260 | rule2tac ctxt subst (Rule.Rls_ rls) = |
260 | rule2tac ctxt subst (Rule.Rls_ rls) = |
261 Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls)) |
261 Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls)) |
262 | rule2tac ctxt _ rule = |
262 | rule2tac ctxt _ rule = |
263 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string_PIDE ctxt rule ^ "\""); |
263 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string ctxt rule ^ "\""); |
264 |
264 |
265 (* try if a rewrite-rule is applicable to a given formula; |
265 (* try if a rewrite-rule is applicable to a given formula; |
266 in case of rule-sets (recursivley) collect all _atomic_ rewrites *) |
266 in case of rule-sets (recursivley) collect all _atomic_ rewrites *) |
267 fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) asm_rls (subst : subst) f (thm' as Rule.Thm (_, thm)) = |
267 fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) asm_rls (subst : subst) f (thm' as Rule.Thm (_, thm)) = |
268 if Auto_Prog.contains_bdv thm |
268 if Auto_Prog.contains_bdv thm |