renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
authorpaulson
Thu Apr 27 12:11:56 2006 +0200 (2006-04-27)
changeset 19481a6205c6203ea
parent 19480 868cf5051ff5
child 19482 9f11af8f7ef9
renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Library/EfficientNat.thy
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/arith_data.ML
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Thu Apr 27 12:11:05 2006 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Thu Apr 27 12:11:56 2006 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4   
     1.5  fun mk_numeral 0 = Const("0",HOLogic.intT)
     1.6     |mk_numeral 1 = Const("1",HOLogic.intT)
     1.7 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
     1.8 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); 
     1.9   
    1.10  (*Transform an Term to an natural number*)	  
    1.11  	  
     2.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Apr 27 12:11:05 2006 +0200
     2.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Apr 27 12:11:56 2006 +0200
     2.3 @@ -182,7 +182,7 @@
     2.4  
     2.5  (** Utilities **)
     2.6  
     2.7 -fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_bin n;
     2.8 +fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n;
     2.9  
    2.10  (*Decodes a binary INTEGER*)
    2.11  fun dest_numeral (Const("0", _)) = 0
     3.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Apr 27 12:11:05 2006 +0200
     3.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Apr 27 12:11:56 2006 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5  (*Utilities*)
     3.6  
     3.7 -fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n;
     3.8 +fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_binum n;
     3.9  
    3.10  (*Decodes a unary or binary numeral to a NATURAL NUMBER*)
    3.11  fun dest_numeral (Const ("0", _)) = 0
     4.1 --- a/src/HOL/Library/EfficientNat.thy	Thu Apr 27 12:11:05 2006 +0200
     4.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu Apr 27 12:11:56 2006 +0200
     4.3 @@ -36,7 +36,7 @@
     4.4  fun term_of_nat 0 = Const ("0", HOLogic.natT)
     4.5    | term_of_nat 1 = Const ("1", HOLogic.natT)
     4.6    | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
     4.7 -      HOLogic.mk_bin (IntInf.fromInt i);
     4.8 +      HOLogic.mk_binum (IntInf.fromInt i);
     4.9  *}
    4.10  attach (test) {*
    4.11  fun gen_nat i = random_range 0 i;
     5.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 27 12:11:05 2006 +0200
     5.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 27 12:11:56 2006 +0200
     5.3 @@ -80,7 +80,7 @@
     5.4   
     5.5  fun mk_numeral 0 = Const("0",HOLogic.intT)
     5.6     |mk_numeral 1 = Const("1",HOLogic.intT)
     5.7 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
     5.8 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); 
     5.9   
    5.10  (*Transform an Term to an natural number*)	  
    5.11  	  
     6.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Apr 27 12:11:05 2006 +0200
     6.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Apr 27 12:11:56 2006 +0200
     6.3 @@ -38,7 +38,7 @@
     6.4  (* translation of integer numeral tokens to and from bitstrings *)
     6.5  
     6.6  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
     6.7 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str))))
     6.8 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (valOf (IntInf.fromString str))))
     6.9    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    6.10  
    6.11  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
     7.1 --- a/src/HOL/arith_data.ML	Thu Apr 27 12:11:05 2006 +0200
     7.2 +++ b/src/HOL/arith_data.ML	Thu Apr 27 12:11:56 2006 +0200
     7.3 @@ -367,7 +367,7 @@
     7.4    let val {discrete, inj_consts, ...} = ArithTheoryData.get sg
     7.5    in decomp2 (sg,discrete,inj_consts) end
     7.6  
     7.7 -fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
     7.8 +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n)
     7.9  
    7.10  end;
    7.11  
     8.1 --- a/src/HOL/hologic.ML	Thu Apr 27 12:11:05 2006 +0200
     8.2 +++ b/src/HOL/hologic.ML	Thu Apr 27 12:11:56 2006 +0200
     8.3 @@ -83,7 +83,7 @@
     8.4    val number_of_const: typ -> term
     8.5    val int_of: int list -> IntInf.int
     8.6    val dest_binum: term -> IntInf.int
     8.7 -  val mk_bin: IntInf.int -> term
     8.8 +  val mk_binum: IntInf.int -> term
     8.9    val bin_of : term -> int list
    8.10    val listT : typ -> typ
    8.11    val mk_list: ('a -> term) -> typ -> 'a list -> term
    8.12 @@ -318,7 +318,7 @@
    8.13    | mk_bit 1 = B1_const
    8.14    | mk_bit _ = sys_error "mk_bit";
    8.15  
    8.16 -fun mk_bin  n =
    8.17 +fun mk_binum n =
    8.18    let
    8.19      fun mk_bit n = if n = 0 then B0_const else B1_const;
    8.20  
    8.21 @@ -341,7 +341,7 @@
    8.22  
    8.23  fun mk_int 0 = Const ("0", intT)
    8.24    | mk_int 1 = Const ("1", intT)
    8.25 -  | mk_int i = number_of_const intT $ mk_bin i;
    8.26 +  | mk_int i = number_of_const intT $ mk_binum i;
    8.27  
    8.28  
    8.29  (* real *)