| changeset 19381 | 6cd8abc7f15b |
| parent 18708 | 4b3dadb4fe33 |
| child 19481 | a6205c6203ea |
--- a/src/HOL/Tools/numeral_syntax.ML Sun Apr 09 18:51:13 2006 +0200 +++ b/src/HOL/Tools/numeral_syntax.ML Sun Apr 09 18:51:15 2006 +0200 @@ -55,8 +55,6 @@ (* theory setup *) val setup = - Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #> - Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #> Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];