equal
deleted
inserted
replaced
207 tactic |
207 tactic |
208 *} |
208 *} |
209 |
209 |
210 ML{*fun my_print_tac ctxt thm = |
210 ML{*fun my_print_tac ctxt thm = |
211 let |
211 let |
212 val _ = warning (str_of_thm ctxt thm) |
212 val _ = warning (str_of_thm_no_vars ctxt thm) |
213 in |
213 in |
214 Seq.single thm |
214 Seq.single thm |
215 end*} |
215 end*} |
216 |
216 |
217 text_raw {* |
217 text_raw {* |
323 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
323 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
324 \end{readmore} |
324 \end{readmore} |
325 |
325 |
326 *} |
326 *} |
327 |
327 |
328 section {* Simple Tactics *} |
328 section {* Simple Tactics\label{sec:simpletacs} *} |
329 |
329 |
330 text {* |
330 text {* |
331 Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful |
331 Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful |
332 for low-level debugging of tactics. It just prints out a message and the current |
332 for low-level debugging of tactics. It just prints out a message and the current |
333 goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state |
333 goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state |
544 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = |
544 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = |
545 let |
545 let |
546 val str_of_params = str_of_cterms context params |
546 val str_of_params = str_of_cterms context params |
547 val str_of_asms = str_of_cterms context asms |
547 val str_of_asms = str_of_cterms context asms |
548 val str_of_concl = str_of_cterm context concl |
548 val str_of_concl = str_of_cterm context concl |
549 val str_of_prems = str_of_thms context prems |
549 val str_of_prems = str_of_thms_no_vars context prems |
550 val str_of_schms = str_of_cterms context (snd schematics) |
550 val str_of_schms = str_of_cterms context (snd schematics) |
551 |
551 |
552 val _ = (warning ("params: " ^ str_of_params); |
552 val _ = (warning ("params: " ^ str_of_params); |
553 warning ("schematics: " ^ str_of_schms); |
553 warning ("schematics: " ^ str_of_schms); |
554 warning ("assumptions: " ^ str_of_asms); |
554 warning ("assumptions: " ^ str_of_asms); |
1141 ML{*fun print_ss ctxt ss = |
1141 ML{*fun print_ss ctxt ss = |
1142 let |
1142 let |
1143 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss |
1143 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss |
1144 |
1144 |
1145 fun name_thm (nm, thm) = |
1145 fun name_thm (nm, thm) = |
1146 " " ^ nm ^ ": " ^ (str_of_thm ctxt thm) |
1146 " " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm) |
1147 fun name_ctrm (nm, ctrm) = |
1147 fun name_ctrm (nm, ctrm) = |
1148 " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) |
1148 " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) |
1149 |
1149 |
1150 val s1 = ["Simplification rules:"] |
1150 val s1 = ["Simplification rules:"] |
1151 val s2 = map name_thm simps |
1151 val s2 = map name_thm simps |