src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

 
 end;
 
 val known_sos_constants =
   [@{term "op ==>"}, @{term "Trueprop"},
-   @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
+   @{term HOL.False}, @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
    @{term "Not"}, @{term "op = :: bool => _"},
    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
    @{term "op = :: real => _"}, @{term "op < :: real => _"},
    @{term "op <= :: real => _"},
    @{term "op + :: real => _"}, @{term "op - :: real => _"},