isabelle: src/HOLCF/HOLCF.thy@4b393520846e (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
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	9	imports Sprod Ssum Up Lift Discrete One Tr
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	huffman
	Sat, 02 Apr 2005 00:33:51 +0200
changeset 15651	4b393520846e
parent 15650	b37dc98fbbc5
child 15742	64eae3513064
permissions	-rw-r--r--