isabelle: src/HOLCF/HOLCF.thy@7dd4eb2c8055 (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
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	12	end