| changeset 21416 | f23e4e75dfd3 |
| parent 20044 | 92cc2f4c7335 |
--- a/src/HOL/Integ/IntDiv_setup.ML Sat Nov 18 00:20:22 2006 +0100 +++ b/src/HOL/Integ/IntDiv_setup.ML Sat Nov 18 00:20:24 2006 +0100 @@ -10,8 +10,8 @@ structure CancelDivModData = struct -val div_name = "Divides.op div"; -val mod_name = "Divides.op mod"; +val div_name = "Divides.div"; +val mod_name = "Divides.mod"; val mk_binop = HOLogic.mk_binop; val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; val dest_sum = Int_Numeral_Simprocs.dest_sum;