src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 56625 54505623a8ef
parent 56536 aefb4a8da31f
child 57889 049e13f616d4
equal deleted inserted replaced
56624:7eed0fee0241 56625:54505623a8ef
   959 
   959 
   960 end;
   960 end;
   961 
   961 
   962 val known_sos_constants =
   962 val known_sos_constants =
   963   [@{term "op ==>"}, @{term "Trueprop"},
   963   [@{term "op ==>"}, @{term "Trueprop"},
   964    @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
   964    @{term HOL.False}, @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
   965    @{term "Not"}, @{term "op = :: bool => _"},
   965    @{term "Not"}, @{term "op = :: bool => _"},
   966    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
   966    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
   967    @{term "op = :: real => _"}, @{term "op < :: real => _"},
   967    @{term "op = :: real => _"}, @{term "op < :: real => _"},
   968    @{term "op <= :: real => _"},
   968    @{term "op <= :: real => _"},
   969    @{term "op + :: real => _"}, @{term "op - :: real => _"},
   969    @{term "op + :: real => _"}, @{term "op - :: real => _"},