| changeset 20713 | 823967ef47f1 |
| parent 20485 | 3078fd2eec7b |
| child 20854 | f9cf9e62d11c |
--- a/src/HOL/Integ/presburger.ML Tue Sep 26 13:34:15 2006 +0200 +++ b/src/HOL/Integ/presburger.ML Tue Sep 26 13:34:16 2006 +0200 @@ -166,10 +166,10 @@ ("Numeral.Min", iT), ("Numeral.number_of", iT --> iT), ("Numeral.number_of", iT --> nT), - ("0", nT), - ("0", iT), - ("1", nT), - ("1", iT), + ("HOL.zero", nT), + ("HOL.zero", iT), + ("HOL.one", nT), + ("HOL.one", iT), ("False", bT), ("True", bT)];