--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 10:56:46 2010 +0200
@@ -1356,7 +1356,7 @@
val known_sos_constants =
[@{term "op ==>"}, @{term "Trueprop"},
- @{term HOL.implies}, @{term "op &"}, @{term "op |"},
+ @{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 => _"},