# HG changeset patch # User wenzelm # Date 1182724594 -7200 # Node ID 881b0497295324fb3a432a309318f517a5e51f76 # Parent 7316582081968ab22b3de1319d57367528c28c77 made type conv pervasive; diff -r 731658208196 -r 881b04972953 src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Mon Jun 25 00:36:33 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Mon Jun 25 00:36:34 2007 +0200 @@ -7,16 +7,16 @@ sig val mk_cnumber : ctyp -> integer -> cterm val mk_cnumeral : integer -> cterm - val semiring_normalize_conv : Proof.context -> Conv.conv - val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> Conv.conv + val semiring_normalize_conv : Proof.context -> conv + val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv val semiring_normalize_tac : Proof.context -> int -> tactic - val semiring_normalize_wrapper : Proof.context -> NormalizerData.entry -> Conv.conv - val semiring_normalize_ord_wrapper : Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) -> Conv.conv + val semiring_normalize_wrapper : Proof.context -> NormalizerData.entry -> conv + val semiring_normalize_ord_wrapper : Proof.context -> NormalizerData.entry -> + (cterm -> cterm -> bool) -> conv val semiring_normalizers_conv : cterm list -> cterm list * thm list -> cterm list * thm list -> - (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> cterm -> bool) -> - {add: Conv.conv, mul: Conv.conv, neg: Conv.conv, main: Conv.conv, - pow: Conv.conv, sub: Conv.conv} + (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> + {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} end structure Normalizer: NORMALIZER = diff -r 731658208196 -r 881b04972953 src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Mon Jun 25 00:36:33 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Mon Jun 25 00:36:34 2007 +0200 @@ -16,7 +16,8 @@ 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} -> morphism -> Context.generic -> Context.generic + conv: morphism -> Proof.context -> cterm -> thm} -> + morphism -> Context.generic -> Context.generic val setup: theory -> theory end;