equal
deleted
inserted
replaced
1 (* Title: HOL/arith_data.ML |
1 (* Title: HOL/arith_data.ML |
2 ID: $Id$ |
|
3 Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow |
2 Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow |
4 |
3 |
5 Basic arithmetic proof tools. |
4 Basic arithmetic proof tools. |
6 *) |
5 *) |
7 |
6 |
8 signature ARITH_DATA = |
7 signature ARITH_DATA = |
9 sig |
8 sig |
10 val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic) |
9 val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm |
11 -> MetaSimplifier.simpset -> term * term -> thm |
10 val simp_all_tac: thm list -> simpset -> tactic |
12 val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic |
|
13 |
11 |
14 val mk_sum: term list -> term |
12 val mk_sum: term list -> term |
15 val mk_norm_sum: term list -> term |
13 val mk_norm_sum: term list -> term |
16 val dest_sum: term -> term list |
14 val dest_sum: term -> term list |
17 |
15 |