src/HOL/Groebner_Basis.thy
changeset 23458 b2267a9e9e28
parent 23389 aaca6a8e5414
child 23477 f4b83f03cac9
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Jun 21 15:42:11 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Jun 21 15:42:12 2007 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4  begin
     1.5  
     1.6  
     1.7 -
     1.8  subsection {* Semiring normalization *}
     1.9  
    1.10  setup NormalizerData.setup
    1.11 @@ -258,7 +257,7 @@
    1.12  
    1.13  method_setup sring_norm = {*
    1.14    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
    1.15 -*} "Semiring_normalizer"
    1.16 +*} "semiring normalizer"
    1.17  
    1.18  
    1.19  locale gb_field = gb_ring +
    1.20 @@ -277,6 +276,7 @@
    1.21  
    1.22  end
    1.23  
    1.24 +
    1.25  subsection {* Groebner Bases *}
    1.26  
    1.27  locale semiringb = gb_semiring +
    1.28 @@ -366,7 +366,6 @@
    1.29      conv = fn phi => K numeral_conv}
    1.30  *}
    1.31  
    1.32 -
    1.33  interpretation natgb: semiringb
    1.34    ["op +" "op *" "op ^" "0::nat" "1"]
    1.35  proof (unfold_locales, simp add: ring_eq_simps power_Suc)
    1.36 @@ -416,7 +415,6 @@
    1.37  end
    1.38  
    1.39  
    1.40 -
    1.41  lemmas bool_simps = simp_thms(1-34)
    1.42  lemma dnf:
    1.43      "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
    1.44 @@ -438,7 +436,7 @@
    1.45  use "Tools/Groebner_Basis/groebner.ML"
    1.46  
    1.47  method_setup algebra =
    1.48 -{* 
    1.49 +{*
    1.50  let
    1.51   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    1.52   val addN = "add"
    1.53 @@ -452,7 +450,6 @@
    1.54   #> (fn ((add_ths, del_ths), ctxt) => 
    1.55         Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.56  end
    1.57 -
    1.58 -*} ""
    1.59 +*} "solve polynomial equations over (semi)rings using Groebner bases"
    1.60  
    1.61  end