isabelle: src/HOL/Lfp.thy@7361ac9b024d (annotated)

1264 3eb91524b938 added local simpsets; removed IOA from 'make test' clasohm parents: 1114 diff changeset	1	(* Title: HOL/Lfp.thy
923 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 1992 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	The Knaster-Tarski Theorem
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
1114 c8dfb56a7e95 Prod is now a parent of Lfp. nipkow parents: 923 diff changeset	9	Lfp = mono + Prod +
1370 7361ac9b024d removed quotes from types in consts and syntax sections clasohm parents: 1264 diff changeset	10	consts lfp :: ['a set=>'a set] => 'a set
923 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	(least fixed point)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13	lfp_def "lfp(f) == Inter({u. f(u) <= u})"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	end

author	clasohm
	Wed, 29 Nov 1995 16:44:59 +0100
changeset 1370	7361ac9b024d
parent 1264	3eb91524b938
child 1475	7f5a4cd08209
permissions	-rw-r--r--