isabelle: src/HOLCF/HOLCF.thy@a53abeedc879 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4
12030 46d57d0290a2 GPLed; wenzelm parents: 3327 diff changeset	5	Top theory for HOLCF system.
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	8	theory HOLCF
15742 64eae3513064 speed improvements for the domain package huffman parents: 15651 diff changeset	9	imports Sprod Ssum Up Lift Discrete One Tr Domain
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	10	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	11
15651 4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	12	text {*
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	13	Remove continuity lemmas from simp set, so continuity subgoals
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	14	are handled by the @{text cont_proc} simplifier procedure.
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	15	*}
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	16	declare cont_lemmas1 [simp del]
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	17	declare cont_lemmas_ext [simp del]
4b393520846e Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used. huffman parents: 15650 diff changeset	18
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	19	end

author	wenzelm
	Tue, 17 May 2005 18:10:36 +0200
changeset 15983	a53abeedc879
parent 15742	64eae3513064
child 16054	b8ba6727712f
permissions	-rw-r--r--