| changeset 226 | cc87161971e4 |
| parent 8 | c3d2c6dcf3f0 |
| child 289 | 78541329ff35 |
| 225:76f60e6400e8 | 226:cc87161971e4 |
|---|---|
1 (* Title: CCL/wf |
1 (* Title: CCL/wfd.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 For wf.thy. |
4 For wfd.thy. |
5 |
5 |
6 Based on |
6 Based on |
7 Titles: ZF/wf.ML and HOL/ex/lex-prod |
7 Titles: ZF/wf.ML and HOL/ex/lex-prod |
8 Authors: Lawrence C Paulson and Tobias Nipkow |
8 Authors: Lawrence C Paulson and Tobias Nipkow |
9 Copyright 1992 University of Cambridge |
9 Copyright 1992 University of Cambridge |