equal
deleted
inserted
replaced
208 tactic |
208 tactic |
209 *} |
209 *} |
210 |
210 |
211 ML{*fun my_print_tac ctxt thm = |
211 ML{*fun my_print_tac ctxt thm = |
212 let |
212 let |
213 val _ = warning (str_of_thm_no_vars ctxt thm) |
213 val _ = writeln (str_of_thm_no_vars ctxt thm) |
214 in |
214 in |
215 Seq.single thm |
215 Seq.single thm |
216 end*} |
216 end*} |
217 |
217 |
218 text_raw {* |
218 text_raw {* |
535 val str_of_asms = str_of_cterms context asms |
535 val str_of_asms = str_of_cterms context asms |
536 val str_of_concl = str_of_cterm context concl |
536 val str_of_concl = str_of_cterm context concl |
537 val str_of_prems = str_of_thms_no_vars context prems |
537 val str_of_prems = str_of_thms_no_vars context prems |
538 val str_of_schms = str_of_cterms context (snd schematics) |
538 val str_of_schms = str_of_cterms context (snd schematics) |
539 |
539 |
540 val _ = (warning ("params: " ^ str_of_params); |
540 val _ = (writeln ("params: " ^ str_of_params); |
541 warning ("schematics: " ^ str_of_schms); |
541 writeln ("schematics: " ^ str_of_schms); |
542 warning ("assumptions: " ^ str_of_asms); |
542 writeln ("assumptions: " ^ str_of_asms); |
543 warning ("conclusion: " ^ str_of_concl); |
543 writeln ("conclusion: " ^ str_of_concl); |
544 warning ("premises: " ^ str_of_prems)) |
544 writeln ("premises: " ^ str_of_prems)) |
545 in |
545 in |
546 no_tac |
546 no_tac |
547 end*} |
547 end*} |
548 text_raw{* |
548 text_raw{* |
549 \end{isabelle} |
549 \end{isabelle} |
581 Notice also that we had to append @{text [quotes] "?"} to the |
581 Notice also that we had to append @{text [quotes] "?"} to the |
582 \isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally |
582 \isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally |
583 expects that the subgoal is solved completely. Since in the function @{ML |
583 expects that the subgoal is solved completely. Since in the function @{ML |
584 sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously |
584 sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously |
585 fails. The question-mark allows us to recover from this failure in a |
585 fails. The question-mark allows us to recover from this failure in a |
586 graceful manner so that the warning messages are not overwritten by an |
586 graceful manner so that the output messages are not overwritten by an |
587 ``empty sequence'' error message. |
587 ``empty sequence'' error message. |
588 |
588 |
589 If we continue the proof script by applying the @{text impI}-rule |
589 If we continue the proof script by applying the @{text impI}-rule |
590 *} |
590 *} |
591 |
591 |
1170 ["Congruences rules:"] @ (map name_thm congs) @ |
1170 ["Congruences rules:"] @ (map name_thm congs) @ |
1171 ["Simproc patterns:"] @ (map name_ctrm procs) |
1171 ["Simproc patterns:"] @ (map name_ctrm procs) |
1172 in |
1172 in |
1173 s |> separate "\n" |
1173 s |> separate "\n" |
1174 |> implode |
1174 |> implode |
1175 |> warning |
1175 |> writeln |
1176 end*} |
1176 end*} |
1177 text_raw {* |
1177 text_raw {* |
1178 \end{isabelle} |
1178 \end{isabelle} |
1179 \end{minipage} |
1179 \end{minipage} |
1180 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing |
1180 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing |
1492 *} |
1492 *} |
1493 |
1493 |
1494 ML %linenosgray{*fun fail_sp_aux simpset redex = |
1494 ML %linenosgray{*fun fail_sp_aux simpset redex = |
1495 let |
1495 let |
1496 val ctxt = Simplifier.the_context simpset |
1496 val ctxt = Simplifier.the_context simpset |
1497 val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex)) |
1497 val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex)) |
1498 in |
1498 in |
1499 NONE |
1499 NONE |
1500 end*} |
1500 end*} |
1501 |
1501 |
1502 text {* |
1502 text {* |
1563 *} |
1563 *} |
1564 |
1564 |
1565 ML{*fun fail_sp_aux' simpset redex = |
1565 ML{*fun fail_sp_aux' simpset redex = |
1566 let |
1566 let |
1567 val ctxt = Simplifier.the_context simpset |
1567 val ctxt = Simplifier.the_context simpset |
1568 val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex)) |
1568 val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex)) |
1569 in |
1569 in |
1570 NONE |
1570 NONE |
1571 end*} |
1571 end*} |
1572 |
1572 |
1573 text {* |
1573 text {* |