equal
deleted
inserted
replaced
53 |
53 |
54 |
54 |
55 (* theory setup *) |
55 (* theory setup *) |
56 |
56 |
57 val setup = |
57 val setup = |
58 Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #> |
|
59 Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #> |
|
60 Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> |
58 Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> |
61 Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; |
59 Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; |
62 |
60 |
63 end; |
61 end; |