864 @{term "op + :: real => _"}, @{term "op - :: real => _"}, |
864 @{term "op + :: real => _"}, @{term "op - :: real => _"}, |
865 @{term "op * :: real => _"}, @{term "uminus :: real => _"}, |
865 @{term "op * :: real => _"}, @{term "uminus :: real => _"}, |
866 @{term "op / :: real => _"}, @{term "inverse :: real => _"}, |
866 @{term "op / :: real => _"}, @{term "inverse :: real => _"}, |
867 @{term "op ^ :: real => _"}, @{term "abs :: real => _"}, |
867 @{term "op ^ :: real => _"}, @{term "abs :: real => _"}, |
868 @{term "min :: real => _"}, @{term "max :: real => _"}, |
868 @{term "min :: real => _"}, @{term "max :: real => _"}, |
869 @{term "0::real"}, @{term "1::real"}, @{term "number_of :: int => real"}, |
869 @{term "0::real"}, @{term "1::real"}, |
870 @{term "number_of :: int => nat"}, |
870 @{term "numeral :: num => nat"}, |
871 @{term "Int.Bit0"}, @{term "Int.Bit1"}, |
871 @{term "numeral :: num => real"}, |
872 @{term "Int.Pls"}, @{term "Int.Min"}]; |
872 @{term "neg_numeral :: num => real"}, |
|
873 @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}]; |
873 |
874 |
874 fun check_sos kcts ct = |
875 fun check_sos kcts ct = |
875 let |
876 let |
876 val t = term_of ct |
877 val t = term_of ct |
877 val _ = if not (null (Term.add_tfrees t []) |
878 val _ = if not (null (Term.add_tfrees t []) |