# HG changeset patch
# User wenzelm
# Date 1182433332 -7200
# Node ID b2267a9e9e28255ab1ba802d0a2000c46ab7ddbf
# Parent  53b788c014f8801acc14b40c068a9ddf1f763cde
tuned comments;

diff -r 53b788c014f8 -r b2267a9e9e28 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Jun 21 15:42:11 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu Jun 21 15:42:12 2007 +0200
@@ -14,7 +14,6 @@
 begin
 
 
-
 subsection {* Semiring normalization *}
 
 setup NormalizerData.setup
@@ -258,7 +257,7 @@
 
 method_setup sring_norm = {*
   Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
-*} "Semiring_normalizer"
+*} "semiring normalizer"
 
 
 locale gb_field = gb_ring +
@@ -277,6 +276,7 @@
 
 end
 
+
 subsection {* Groebner Bases *}
 
 locale semiringb = gb_semiring +
@@ -366,7 +366,6 @@
     conv = fn phi => K numeral_conv}
 *}
 
-
 interpretation natgb: semiringb
   ["op +" "op *" "op ^" "0::nat" "1"]
 proof (unfold_locales, simp add: ring_eq_simps power_Suc)
@@ -416,7 +415,6 @@
 end
 
 
-
 lemmas bool_simps = simp_thms(1-34)
 lemma dnf:
     "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
@@ -438,7 +436,7 @@
 use "Tools/Groebner_Basis/groebner.ML"
 
 method_setup algebra =
-{* 
+{*
 let
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
  val addN = "add"
@@ -452,7 +450,6 @@
  #> (fn ((add_ths, del_ths), ctxt) => 
        Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
 end
-
-*} ""
+*} "solve polynomial equations over (semi)rings using Groebner bases"
 
 end