src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 47108 2a1953f0d20d
parent 46497 89ccf66aa73d
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -866,10 +866,11 @@
     1.4     @{term "op / :: real => _"}, @{term "inverse :: real => _"},
     1.5     @{term "op ^ :: real => _"}, @{term "abs :: real => _"},
     1.6     @{term "min :: real => _"}, @{term "max :: real => _"},
     1.7 -   @{term "0::real"}, @{term "1::real"}, @{term "number_of :: int => real"},
     1.8 -   @{term "number_of :: int => nat"},
     1.9 -   @{term "Int.Bit0"}, @{term "Int.Bit1"},
    1.10 -   @{term "Int.Pls"}, @{term "Int.Min"}];
    1.11 +   @{term "0::real"}, @{term "1::real"},
    1.12 +   @{term "numeral :: num => nat"},
    1.13 +   @{term "numeral :: num => real"},
    1.14 +   @{term "neg_numeral :: num => real"},
    1.15 +   @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
    1.16  
    1.17  fun check_sos kcts ct =
    1.18   let