46 fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis |
46 fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis |
47 fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm) |
47 fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm) |
48 | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm) |
48 | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm) |
49 | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_) |
49 | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_) |
50 |
50 |
51 fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) = |
51 fun make_single ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = |
52 (Tactic.Rewrite (id, thm), |
52 (Tactic.Rewrite (id, thm), |
53 Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)), |
53 Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule r, t, (t', a)), |
54 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) |
54 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) |
55 | make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) = |
55 | make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) = |
56 (Tactic.Rewrite_Set (Rule_Set.id_from_rule r), |
56 (Tactic.Rewrite_Set (Rule_Set.id_from_rule r), |
57 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)), |
57 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)), |
58 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) |
58 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) |