32 # the latter problem may be resolved automatically if "fun autocalc" is |
32 # the latter problem may be resolved automatically if "fun autocalc" is |
33 not any more used for the specify-phase and for changing the phases*) |
33 not any more used for the specify-phase and for changing the phases*) |
34 type single = |
34 type single = |
35 (Tactic.input * (* for comparison with input tac *) |
35 (Tactic.input * (* for comparison with input tac *) |
36 Tactic.T * (* for ctree generation *) |
36 Tactic.T * (* for ctree generation *) |
37 (Pos.pos' * (* after applying tac_, for ctree generation *) |
37 (Pos.pos' * (* after applying tac_, for ctree generation *) |
38 (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *) |
38 (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *) |
39 val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single |
39 val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single |
40 fun taci2str ((tac, tac_, (pos', (istate, _))):single) = |
40 fun taci2str ((tac, tac_, (pos', (istate, _))):single) = |
41 "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^ |
41 "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^ |
42 Istate_Def.string_of istate ^ " ))" |
42 Istate_Def.string_of istate ^ " ))" |