536 \begin{minipage}{\textwidth} |
536 \begin{minipage}{\textwidth} |
537 \begin{isabelle} |
537 \begin{isabelle} |
538 *} |
538 *} |
539 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = |
539 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = |
540 let |
540 let |
541 val str_of_params = str_of_cterms context params |
541 val string_of_params = string_of_cterms context params |
542 val str_of_asms = str_of_cterms context asms |
542 val string_of_asms = string_of_cterms context asms |
543 val str_of_concl = str_of_cterm context concl |
543 val string_of_concl = string_of_cterm context concl |
544 val str_of_prems = str_of_thms_no_vars context prems |
544 val string_of_prems = string_of_thms_no_vars context prems |
545 val str_of_schms = str_of_cterms context (snd schematics) |
545 val string_of_schms = string_of_cterms context (snd schematics) |
546 |
546 |
547 val _ = (writeln ("params: " ^ str_of_params); |
547 val _ = (writeln ("params: " ^ string_of_params); |
548 writeln ("schematics: " ^ str_of_schms); |
548 writeln ("schematics: " ^ string_of_schms); |
549 writeln ("assumptions: " ^ str_of_asms); |
549 writeln ("assumptions: " ^ string_of_asms); |
550 writeln ("conclusion: " ^ str_of_concl); |
550 writeln ("conclusion: " ^ string_of_concl); |
551 writeln ("premises: " ^ str_of_prems)) |
551 writeln ("premises: " ^ string_of_prems)) |
552 in |
552 in |
553 no_tac |
553 no_tac |
554 end*} |
554 end*} |
555 text_raw{* |
555 text_raw{* |
556 \end{isabelle} |
556 \end{isabelle} |
1180 ML{*fun print_ss ctxt ss = |
1180 ML{*fun print_ss ctxt ss = |
1181 let |
1181 let |
1182 val {simps, congs, procs, ...} = Simplifier.dest_ss ss |
1182 val {simps, congs, procs, ...} = Simplifier.dest_ss ss |
1183 |
1183 |
1184 fun name_thm (nm, thm) = |
1184 fun name_thm (nm, thm) = |
1185 " " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm) |
1185 " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm) |
1186 fun name_ctrm (nm, ctrm) = |
1186 fun name_ctrm (nm, ctrm) = |
1187 " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) |
1187 " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm) |
1188 |
1188 |
1189 val s = ["Simplification rules:"] @ map name_thm simps @ |
1189 val s = ["Simplification rules:"] @ map name_thm simps @ |
1190 ["Congruences rules:"] @ map name_thm congs @ |
1190 ["Congruences rules:"] @ map name_thm congs @ |
1191 ["Simproc patterns:"] @ map name_ctrm procs |
1191 ["Simproc patterns:"] @ map name_ctrm procs |
1192 in |
1192 in |
1495 (FIXME: @{ML ObjectLogic.full_atomize_tac}, |
1495 (FIXME: @{ML ObjectLogic.full_atomize_tac}, |
1496 @{ML ObjectLogic.rulify_tac}) |
1496 @{ML ObjectLogic.rulify_tac}) |
1497 |
1497 |
1498 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) |
1498 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) |
1499 |
1499 |
|
1500 (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.) |
|
1501 |
1500 *} |
1502 *} |
1501 |
1503 |
1502 section {* Simprocs *} |
1504 section {* Simprocs *} |
1503 |
1505 |
1504 text {* |
1506 text {* |