equal
deleted
inserted
replaced
549 val string_of_asms = string_of_cterms context asms |
549 val string_of_asms = string_of_cterms context asms |
550 val string_of_concl = string_of_cterm context concl |
550 val string_of_concl = string_of_cterm context concl |
551 val string_of_prems = string_of_thms_no_vars context prems |
551 val string_of_prems = string_of_thms_no_vars context prems |
552 val string_of_schms = string_of_cterms context (map fst (snd schematics)) |
552 val string_of_schms = string_of_cterms context (map fst (snd schematics)) |
553 |
553 |
554 val _ = (tracing ("params: " ^ string_of_params); |
554 val strs = ["params: " ^ string_of_params, |
555 tracing ("schematics: " ^ string_of_schms); |
555 "schematics: " ^ string_of_schms, |
556 tracing ("assumptions: " ^ string_of_asms); |
556 "assumptions: " ^ string_of_asms, |
557 tracing ("conclusion: " ^ string_of_concl); |
557 "conclusion: " ^ string_of_concl, |
558 tracing ("premises: " ^ string_of_prems)) |
558 "premises: " ^ string_of_prems] |
559 in |
559 in |
560 all_tac |
560 tracing (cat_lines strs); all_tac |
561 end*} |
561 end*} |
562 |
562 |
563 text_raw{* |
563 text_raw{* |
564 \end{isabelle} |
564 \end{isabelle} |
565 \end{minipage} |
565 \end{minipage} |