equal
deleted
inserted
replaced
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68. |
6 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68. |
7 *) |
7 *) |
8 |
8 |
9 (* ML bindings *) |
9 (* legacy ML bindings *) |
10 |
10 |
11 val plusI = thm "plusI"; |
11 val plusI = thm "plusI"; |
12 val minusI = thm "minusI"; |
12 val minusI = thm "minusI"; |
13 val timesI = thm "timesI"; |
13 val timesI = thm "timesI"; |
14 val eq_reflection = thm "eq_reflection"; |
14 val eq_reflection = thm "eq_reflection"; |