# 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 **)