src/HOL/Integ/presburger.ML
changeset 15013 34264f5e4691
parent 14981 e73f8140af78
child 15240 e1e6db03beee
--- a/src/HOL/Integ/presburger.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -120,9 +120,9 @@
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
 
-   ("Numeral.bin.Bit", binT --> bT --> binT),
-   ("Numeral.bin.Pls", binT),
-   ("Numeral.bin.Min", binT),
+   ("Numeral.Bit", binT --> bT --> binT),
+   ("Numeral.Pls", binT),
+   ("Numeral.Min", binT),
    ("Numeral.number_of", binT --> iT),
    ("Numeral.number_of", binT --> nT),
    ("0", nT),