src/HOL/Rat.thy
changeset 55974 c835a9379026
parent 55143 04448228381d
child 56409 36489d77c484
     1.1 --- a/src/HOL/Rat.thy	Fri Mar 07 11:41:25 2014 +0100
     1.2 +++ b/src/HOL/Rat.thy	Fri Mar 07 11:46:26 2014 +0100
     1.3 @@ -1155,12 +1155,16 @@
     1.4        let
     1.5          fun mk 1 = Syntax.const @{const_syntax Num.One}
     1.6            | mk i =
     1.7 -              let val (q, r) = Integer.div_mod i 2
     1.8 -              in HOLogic.mk_bit r $ (mk q) end;
     1.9 +              let
    1.10 +                val (q, r) = Integer.div_mod i 2;
    1.11 +                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
    1.12 +              in Syntax.const bit $ (mk q) end;
    1.13        in
    1.14          if i = 0 then Syntax.const @{const_syntax Groups.zero}
    1.15          else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
    1.16 -        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
    1.17 +        else
    1.18 +          Syntax.const @{const_syntax Groups.uminus} $
    1.19 +            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
    1.20        end;
    1.21  
    1.22      fun mk_frac str =
    1.23 @@ -1181,6 +1185,7 @@
    1.24  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
    1.25    by simp
    1.26  
    1.27 +
    1.28  subsection {* Hiding implementation details *}
    1.29  
    1.30  hide_const (open) normalize positive