# HG changeset patch
# User wenzelm
# Date 1753036264 -7200
# Node ID 051177553f16aca669e2951609a8f71e11db9781
# Parent  e5db7672d1923dd1b0972b0467f6981e0d07a7a2
more diagnostic operations;

diff -r e5db7672d192 -r 051177553f16 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sun Jul 20 19:06:21 2025 +0200
+++ b/src/Pure/bires.ML	Sun Jul 20 20:31:04 2025 +0200
@@ -59,6 +59,7 @@
 
   type netpair = (tag * rule) Net.net * (tag * rule) Net.net
   val empty_netpair: netpair
+  val pretty_netpair: Proof.context -> string -> netpair -> Pretty.T list
   val insert_tagged_rule: tag * rule -> netpair -> netpair
   val delete_tagged_rule: int * thm -> netpair -> netpair
 
@@ -241,6 +242,17 @@
 
 val empty_netpair: netpair = (Net.empty, Net.empty);
 
+fun pretty_netpair ctxt title (inet, enet) =
+  let
+    fun pretty_entry ({weight, ...}: tag, (_, thm): rule) =
+      Pretty.item [Pretty.str (string_of_int weight), Pretty.brk 1, Thm.pretty_thm ctxt thm];
+
+    fun pretty_net elim net =
+      (case Net.content net |> sort_distinct (tag_ord o apply2 #1) |> map pretty_entry of
+        [] => NONE
+      | prts => SOME (Pretty.big_list (title ^ " " ^ (if elim then "elim" else "intro")) prts));
+  in map_filter I [pretty_net false inet, pretty_net true enet] end;
+
 
 (** Natural Deduction using (bires_flg, rule) pairs **)