# HG changeset patch
# User haftmann
# Date 1273158558 -7200
# Node ID 61c4290d002f630a4579286313141c1907c99a0b
# Parent  999e2d8603c25ecc01decca76cfb1dcc7b8f059a
tuned whitespace

diff -r 999e2d8603c2 -r 61c4290d002f src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 17:06:47 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 17:09:18 2010 +0200
@@ -10,24 +10,24 @@
   val get: Proof.context -> (thm * entry) list
   val match: Proof.context -> cterm -> entry option
   val del: attribute
-  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
-    -> attribute
+  val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
+    field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
   val funs: thm -> {is_const: morphism -> cterm -> bool,
     dest_const: morphism -> cterm -> Rat.rat,
     mk_const: morphism -> ctyp -> Rat.rat -> cterm,
     conv: morphism -> Proof.context -> cterm -> thm} -> declaration
 
-  val semiring_normalize_conv : Proof.context -> conv
-  val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
-  val semiring_normalize_wrapper :  Proof.context -> entry -> conv
-  val semiring_normalize_ord_wrapper :  Proof.context -> entry ->
-    (cterm -> cterm -> bool) -> conv
-  val semiring_normalizers_conv :
-    cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
+  val semiring_normalize_conv: Proof.context -> conv
+  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
+  val semiring_normalize_wrapper: Proof.context -> entry -> conv
+  val semiring_normalize_ord_wrapper: Proof.context -> entry
+    -> (cterm -> cterm -> bool) -> conv
+  val semiring_normalizers_conv: cterm list -> cterm list * thm list
+    -> cterm list * thm list -> cterm list * thm list ->
       (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
         {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
-  val semiring_normalizers_ord_wrapper :  
-    Proof.context -> entry -> (cterm -> cterm -> bool) ->
+  val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
+    (cterm -> cterm -> bool) ->
       {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
 
   val setup: theory -> theory