# HG changeset patch
# User wenzelm
# Date 1751806788 -7200
# Node ID f7a6b012600e5b092d739143b56e7f80b60ad8da
# Parent  c6b3f0ee0a69220f611db352520b95f5b873c5b9
tuned comments;

diff -r c6b3f0ee0a69 -r f7a6b012600e src/Pure/bires.ML
--- 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;