isabelle: src/HOL/Gfp.thy@6960ec882bca (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/gfp.thy
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1994 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6	Greatest fixed points (requires Lfp too!)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	9	Gfp = Lfp +
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10	consts gfp :: "['a set=>'a set] => 'a set"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	11	defs
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12	(greatest fixed point)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13	gfp_def "gfp(f) == Union({u. u <= f(u)})"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	end

author	regensbu
	Fri, 06 Oct 1995 16:17:08 +0100
changeset 1273	6960ec882bca
parent 923	ff1574a81019
child 1370	7361ac9b024d
permissions	-rw-r--r--