equal
deleted
inserted
replaced
1 (* Title: HOL/HOL.ML |
1 (* Title: HOL/HOL.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 For HOL.thy |
|
7 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 |
8 *) |
7 *) |
9 |
|
10 open HOL; |
|
11 |
8 |
12 |
9 |
13 (** Equality **) |
10 (** Equality **) |
14 section "="; |
11 section "="; |
15 |
12 |