src/HOL/Tools/Groebner_Basis/normalizer.ML
changeset 23559 0de527730294
parent 23485 881b04972953
child 23580 998a6fda9bb6
equal deleted inserted replaced
23558:9325845aff1c 23559:0de527730294
    19        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    19        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    20 end
    20 end
    21 
    21 
    22 structure Normalizer: NORMALIZER = 
    22 structure Normalizer: NORMALIZER = 
    23 struct
    23 struct
    24 open Misc;
    24 
       
    25 open Conv Misc;
    25 
    26 
    26 local
    27 local
    27  val pls_const = @{cterm "Numeral.Pls"}
    28  val pls_const = @{cterm "Numeral.Pls"}
    28    and min_const = @{cterm "Numeral.Min"}
    29    and min_const = @{cterm "Numeral.Min"}
    29    and bit_const = @{cterm "Numeral.Bit"}
    30    and bit_const = @{cterm "Numeral.Bit"}