author | clasohm |
Fri, 22 Oct 1993 13:44:27 +0100 | |
changeset 76 | c616d66c640e |
parent 0 | a5a9c433f639 |
child 120 | 09287f26bfb8 |
permissions | -rw-r--r-- |
(* Title: ZF/ex/llist-fn.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Functions for Lazy Lists in Zermelo-Fraenkel Set Theory *) LListFn = LList + consts lconst :: "i => i" rules lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))" end