src/HOL/IntDiv.thy
changeset 31068 f591144b0f17
parent 31065 d87465cbfc9e
child 31662 57f7ef0dba8e
     1.1 --- a/src/HOL/IntDiv.thy	Fri May 08 08:01:09 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Fri May 08 09:48:07 2009 +0200
     1.3 @@ -252,8 +252,8 @@
     1.4    val div_name = @{const_name div};
     1.5    val mod_name = @{const_name mod};
     1.6    val mk_binop = HOLogic.mk_binop;
     1.7 -  val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
     1.8 -  val dest_sum = Int_Numeral_Simprocs.dest_sum;
     1.9 +  val mk_sum = Numeral_Simprocs.mk_sum HOLogic.intT;
    1.10 +  val dest_sum = Numeral_Simprocs.dest_sum;
    1.11  
    1.12    val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
    1.13