equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 structure CancelDivModData = |
10 structure CancelDivModData = |
11 struct |
11 struct |
12 |
12 |
13 val div_name = "Divides.op div"; |
13 val div_name = "Divides.div"; |
14 val mod_name = "Divides.op mod"; |
14 val mod_name = "Divides.mod"; |
15 val mk_binop = HOLogic.mk_binop; |
15 val mk_binop = HOLogic.mk_binop; |
16 val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; |
16 val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; |
17 val dest_sum = Int_Numeral_Simprocs.dest_sum; |
17 val dest_sum = Int_Numeral_Simprocs.dest_sum; |
18 |
18 |
19 (*logic*) |
19 (*logic*) |