hide consts in Numeral.thy;
authorwenzelm
Sun Apr 09 18:51:15 2006 +0200 (2006-04-09)
changeset 193816cd8abc7f15b
parent 19380 b808efaa5828
child 19382 44937faf9e1a
hide consts in Numeral.thy;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sun Apr 09 18:51:13 2006 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sun Apr 09 18:51:15 2006 +0200
     1.3 @@ -55,8 +55,6 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val setup =
     1.7 -  Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
     1.8 -  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
     1.9    Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    1.10    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
    1.11