src/HOL/Tools/numeral_syntax.ML
changeset 18708 4b3dadb4fe33
parent 16365 838c65dad23a
child 19381 6cd8abc7f15b
equal deleted inserted replaced
18707:9d6154f76476 18708:4b3dadb4fe33
     6 theory HOL/Numeral.
     6 theory HOL/Numeral.
     7 *)
     7 *)
     8 
     8 
     9 signature NUMERAL_SYNTAX =
     9 signature NUMERAL_SYNTAX =
    10 sig
    10 sig
    11   val setup: (theory -> theory) list
    11   val setup: theory -> theory
    12 end;
    12 end;
    13 
    13 
    14 structure NumeralSyntax: NUMERAL_SYNTAX =
    14 structure NumeralSyntax: NUMERAL_SYNTAX =
    15 struct
    15 struct
    16 
    16 
    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"],
    58   Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
    59   Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"],
    59   Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
    60    Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    60   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    61   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    61   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
    62 
    62 
    63 end;
    63 end;