# HG changeset patch
# User haftmann
# Date 1273158407 -7200
# Node ID 999e2d8603c25ecc01decca76cfb1dcc7b8f059a
# Parent  f7329e6734bd80001b4eb36cfeb98f58c1286df2
tuned headings

diff -r f7329e6734bd -r 999e2d8603c2 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 17:02:34 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 17:06:47 2010 +0200
@@ -170,7 +170,7 @@
   in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
 
 
-(* Very basic stuff for terms *)
+(** auxiliary **)
 
 fun is_comb ct =
   (case Thm.term_of ct of
@@ -216,7 +216,10 @@
 val true_tm = @{cterm "True"};
 
 
-(* The main function! *)
+(** normalizing conversions **)
+
+(* core conversion *)
+
 fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
   (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
 let
@@ -784,6 +787,9 @@
 
 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
 
+
+(* various normalizing conversions *)
+
 fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
                                      {conv, dest_const, mk_const, is_const}) ord =
   let