Old_HOL: Lfp.thy@093e273405f0 (annotated)

0 7949f97df77a Initial revision clasohm parents: diff changeset	1	(* Title: HOL/lfp.thy
7949f97df77a Initial revision clasohm parents: diff changeset	2	ID: $Id$
7949f97df77a Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7949f97df77a Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
7949f97df77a Initial revision clasohm parents: diff changeset	5
7949f97df77a Initial revision clasohm parents: diff changeset	6	The Knaster-Tarski Theorem
7949f97df77a Initial revision clasohm parents: diff changeset	7	*)
7949f97df77a Initial revision clasohm parents: diff changeset	8
116 ab4328bbff70 HOL/subset.thy, equalities.thy, mono.thy: new lcp parents: 0 diff changeset	9	Lfp = mono +
0 7949f97df77a Initial revision clasohm parents: diff changeset	10	consts lfp :: "['a set=>'a set] => 'a set"
178 12dd5d2e266b rules -> defs nipkow parents: 116 diff changeset	11	defs
0 7949f97df77a Initial revision clasohm parents: diff changeset	12	(least fixed point)
7949f97df77a Initial revision clasohm parents: diff changeset	13	lfp_def "lfp(f) == Inter({u. f(u) <= u})"
7949f97df77a Initial revision clasohm parents: diff changeset	14	end