src/HOL/Tools/Qelim/cooper_data.ML
changeset 34974 18b41bba42b5
parent 33519 e31a85f92ce9
child 36715 5f612b6d64a8
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -33,7 +33,7 @@
    @{term "abs :: int => _"},
    @{term "max :: int => _"}, @{term "max :: nat => _"},
    @{term "min :: int => _"}, @{term "min :: nat => _"},
-   @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
+   @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
    @{term "Not"}, @{term "Suc"},
    @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
    @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},