src/HOL/Tools/numeral_syntax.ML
changeset 13491 ddf6ae639f21
parent 13110 ca8cd110f769
child 13495 af27202d6d1c
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Aug 12 17:48:15 2002 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon Aug 12 17:48:19 2002 +0200
     1.3 @@ -29,14 +29,10 @@
     1.4    | prefix_len pred (x :: xs) =
     1.5        if pred x then 1 + prefix_len pred xs else 0;
     1.6  
     1.7 -(*we consider all "spellings"; Min is likely to be declared elsewhere*)
     1.8 -fun bin_of (Const ("Pls", _)) = []
     1.9 -  | bin_of (Const ("bin.Pls", _)) = []
    1.10 +fun bin_of (Const ("bin.Pls", _)) = []
    1.11    | bin_of (Const ("Numeral.bin.Pls", _)) = []
    1.12 -  | bin_of (Const ("Min", _)) = [~1]
    1.13    | bin_of (Const ("bin.Min", _)) = [~1]
    1.14    | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
    1.15 -  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.16    | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.17    | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    1.18    | bin_of _ = raise Match;
    1.19 @@ -78,7 +74,9 @@
    1.20  (* theory setup *)
    1.21  
    1.22  val setup =
    1.23 - [Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.24 + [Theory.hide_consts false
    1.25 +    ["Numeral.bin.Pls", "Numeral.bin.Min"],
    1.26 +Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.27    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    1.28  
    1.29