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

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	1	(* Title: HOL/gfp.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
923 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
14169 0590de71a016 Converted to new style theories. skalberg parents: 8882 diff changeset	9	theory Gfp = Lfp:
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	10
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	11	constdefs
14169 0590de71a016 Converted to new style theories. skalberg parents: 8882 diff changeset	12	gfp :: "['a set=>'a set] => 'a set"
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	13	"gfp(f) == Union({u. u <= f(u)})" (greatest fixed point)
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	14
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	15	end

author	paulson
	Thu, 05 Feb 2004 10:45:28 +0100
changeset 14377	f454b3004f8f
parent 14169	0590de71a016
child 15131	c69542757a4d
permissions	-rw-r--r--