isabelle: src/ZF/ex/LListFn.thy@a5a9c433f639 (annotated)

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