# 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