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

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.thy
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	2	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	4	HOLCF -- a semantic extension of HOL by the LCF logic.
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	7	theory HOLCF
29130 685c9e05a6ab new theory Dsum: cpo of disjoint sum huffman parents: 28892 diff changeset	8	imports
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	9	Main
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	10	Domain
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	11	Powerdomains
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	12	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	13
40497 d2e876d6da8c rename class 'bifinite' to 'domain' huffman parents: 40431 diff changeset	14	default_sort "domain"
25904 8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	15
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 36452 diff changeset	16	ML {* path_add "~~/src/HOLCF/Library" *}
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 36452 diff changeset	17
40002 c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	18	text {* Legacy theorem names deprecated after Isabelle2009-2: *}
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	19
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	20	lemmas expand_fun_below = fun_below_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	21	lemmas below_fun_ext = fun_belowI
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	22	lemmas expand_cfun_eq = cfun_eq_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	23	lemmas ext_cfun = cfun_eqI
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	24	lemmas expand_cfun_below = cfun_below_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	25	lemmas below_cfun_ext = cfun_belowI
40011 b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	26	lemmas monofun_fun_fun = fun_belowD
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	27	lemmas monofun_fun_arg = monofunE
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	28	lemmas monofun_lub_fun = adm_monofun [THEN admD]
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	29	lemmas cont_lub_fun = adm_cont [THEN admD]
40326 73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	30	lemmas cont2cont_Rep_CFun = cont2cont_APP
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	31	lemmas cont_Rep_CFun_app = cont_APP_app
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	32	lemmas cont_Rep_CFun_app_app = cont_APP_app_app
40002 c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	33
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	34	end

author	wenzelm
	Sat, 27 Nov 2010 14:32:08 +0100
changeset 40742	dc6439c0b8b1
parent 40497	d2e876d6da8c
child 40771	1c6f7d4b110e
permissions	-rw-r--r--