changeset 35762 | af3ff2ba4c54 |
parent 24893 | b8ef7afe3a6b |
child 45602 | 2a858377c3d2 |
35761:c4a698ee83b4 | 35762:af3ff2ba4c54 |
---|---|
1 (* Title: ZF/WF.thy |
1 (* Title: ZF/WF.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Lawrence C Paulson |
2 Author: Tobias Nipkow and Lawrence C Paulson |
4 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
5 |
4 |
6 Derived first for transitive relations, and finally for arbitrary WF relations |
5 Derived first for transitive relations, and finally for arbitrary WF relations |
7 via wf_trancl and trans_trancl. |
6 via wf_trancl and trans_trancl. |