equal
deleted
inserted
replaced
308 val predfun_elim_of = #elim ooo the_predfun_data |
308 val predfun_elim_of = #elim ooo the_predfun_data |
309 |
309 |
310 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data |
310 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data |
311 |
311 |
312 val intros_graph_of = |
312 val intros_graph_of = |
313 Graph.map_nodes (#intros o rep_pred_data) o PredData.get o ProofContext.theory_of |
313 Graph.map (K (#intros o rep_pred_data)) o PredData.get o ProofContext.theory_of |
314 |
314 |
315 (* diagnostic display functions *) |
315 (* diagnostic display functions *) |
316 |
316 |
317 fun print_modes options modes = |
317 fun print_modes options modes = |
318 if show_modes options then |
318 if show_modes options then |