| changeset 0 | a5a9c433f639 |
| child 120 | 09287f26bfb8 |
| -1:000000000000 | 0:a5a9c433f639 |
|---|---|
1 (* Title: ZF/ex/llist-fn.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 LListFn = LList + |
|
10 consts |
|
11 lconst :: "i => i" |
|
12 |
|
13 rules |
|
14 lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))" |
|
15 |
|
16 end |