382 | Free_Solve' => "Free_Solve'" |
382 | Free_Solve' => "Free_Solve'" |
383 |
383 |
384 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*) |
384 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*) |
385 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*) |
385 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*) |
386 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*) |
386 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*) |
387 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ |
387 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^ |
388 "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))" |
388 ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ ", " ^ UnparseC.terms asm ^ "))" |
389 | End_Detail' _ => "End_Detail' xxx" |
389 | End_Detail' _ => "End_Detail' xxx" |
390 |
390 |
391 | Derive' rls => "Derive' " ^ Rule_Set.id rls |
391 | Derive' rls => "Derive' " ^ Rule_Set.id rls |
392 | Calculate' _ => "Calculate' " |
392 | Calculate' _ => "Calculate' " |
393 | Substitute' _ => "Substitute' "(*^(subs2str subs)*) |
393 | Substitute' _ => "Substitute' "(*^(subs2str subs)*) |
395 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*) |
395 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*) |
396 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => |
396 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => |
397 "Subproblem' "(*^(pair2str (domID, strs2str ,))*) |
397 "Subproblem' "(*^(pair2str (domID, strs2str ,))*) |
398 |
398 |
399 | Empty_Tac_ => "Empty_Tac_" |
399 | Empty_Tac_ => "Empty_Tac_" |
400 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")" |
400 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ ", " ^ id ^ ", " ^ result ^ ")" |
401 |
401 |
402 | Begin_Trans' _ => "Begin_Trans' xxx" |
402 | Begin_Trans' _ => "Begin_Trans' xxx" |
403 | End_Trans' _ => "End_Trans' xxx" |
403 | End_Trans' _ => "End_Trans' xxx" |
404 | End_Proof'' => "End_Trans' xxx" |
404 | End_Proof'' => "End_Trans' xxx" |
405 | _ => "string_of not impl. for arg"; |
405 | _ => "string_of not impl. for arg"; |