equal
deleted
inserted
replaced
48 val rev_digs = bin_of tm; |
48 val rev_digs = bin_of tm; |
49 val (sign, zs) = |
49 val (sign, zs) = |
50 (case rev rev_digs of |
50 (case rev rev_digs of |
51 ~1 :: bs => ("-", prefix_len (equal 1) bs) |
51 ~1 :: bs => ("-", prefix_len (equal 1) bs) |
52 | bs => ("", prefix_len (equal 0) bs)); |
52 | bs => ("", prefix_len (equal 0) bs)); |
53 val num = string_of_int (abs (HOLogic.int_of rev_digs)); |
53 val i = HOLogic.int_of rev_digs; |
54 in "#" ^ sign ^ implode (replicate zs "0") ^ num end; |
54 val num = string_of_int (abs i); |
|
55 in |
|
56 if i = 0 orelse i = 1 then raise Match |
|
57 else sign ^ implode (replicate zs "0") ^ num |
|
58 end; |
55 |
59 |
56 |
60 |
57 (* translation of integer numeral tokens to and from bitstrings *) |
61 (* translation of integer numeral tokens to and from bitstrings *) |
58 |
62 |
59 fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] = |
63 fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] = |