equal
deleted
inserted
replaced
1 (* Title: Provers/Arith/cancel_data.ML |
1 (* Title: HOL/Library/Cancellation/cancel_data.ML |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Mathias Fleury, MPII |
3 Author: Mathias Fleury, MPII |
3 Copyright 2017 |
|
4 |
|
5 Based on: |
|
6 Title: Tools/nat_numeral_simprocs.ML |
|
7 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
8 |
4 |
9 Datastructure for the cancelation simprocs. |
5 Datastructure for the cancelation simprocs. |
|
6 *) |
10 |
7 |
11 *) |
|
12 signature CANCEL_DATA = |
8 signature CANCEL_DATA = |
13 sig |
9 sig |
14 val mk_sum : typ -> term list -> term |
10 val mk_sum : typ -> term list -> term |
15 val dest_sum : term -> term list |
11 val dest_sum : term -> term list |
16 val mk_coeff : int * term -> term |
12 val mk_coeff : int * term -> term |