--- a/src/Pure/bires.ML Sun Jul 06 14:58:00 2025 +0200
+++ b/src/Pure/bires.ML Sun Jul 06 14:59:48 2025 +0200
@@ -89,7 +89,7 @@
val empty_netpair: netpair = (Net.empty, Net.empty);
-(** To preserve the order of the rules, tag them with increasing integers **)
+(** To preserve the order of the rules, tag them with decreasing integers **)
(*insert one tagged brl into the pair of nets*)
fun insert_tagged_rule (tagged_rule as (_, (eres, th))) ((inet, enet): netpair) =
@@ -172,7 +172,7 @@
in a ^ " rules " ^ b end;
-(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
+(** Simpler version for resolve_tac -- only one net, and no hyps **)
type net = (int * thm) Net.net;