isabelle: src/HOLCF/Cont.ML@efb95d0d01f7 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	2	(* legacy ML bindings *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	4	val monofun = thm "monofun";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	5	val contlub = thm "contlub";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	6	val cont = thm "cont";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	7	val contlubI = thm "contlubI";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	8	val contlubE = thm "contlubE";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	9	val contI = thm "contI";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	10	val contE = thm "contE";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	11	val monofunI = thm "monofunI";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	12	val monofunE = thm "monofunE";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	13	val ch2ch_monofun = thm "ch2ch_monofun";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	14	val ub2ub_monofun = thm "ub2ub_monofun";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	15	val monocontlub2cont = thm "monocontlub2cont";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	16	val binchain_cont = thm "binchain_cont";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	17	val cont2mono = thm "cont2mono";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	18	val cont2contlub = thm "cont2contlub";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	19	val monofun_finch2finch = thm "monofun_finch2finch";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	20	val cont_finch2finch = thm "cont_finch2finch";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	21	val ch2ch_MF2L = thm "ch2ch_MF2L";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	22	val ch2ch_MF2R = thm "ch2ch_MF2R";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	23	val ch2ch_MF2LR = thm "ch2ch_MF2LR";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	24	val ch2ch_lubMF2R = thm "ch2ch_lubMF2R";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	25	val ch2ch_lubMF2L = thm "ch2ch_lubMF2L";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	26	val lub_MF2_mono = thm "lub_MF2_mono";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	27	val ex_lubMF2 = thm "ex_lubMF2";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	28	val diag_lubMF2_1 = thm "diag_lubMF2_1";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	29	val diag_lubMF2_2 = thm "diag_lubMF2_2";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	30	val contlub_CF2 = thm "contlub_CF2";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	31	val monofun_fun_fun = thm "monofun_fun_fun";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	32	val monofun_fun_arg = thm "monofun_fun_arg";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	33	val mono2mono_MF1L = thm "mono2mono_MF1L";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	34	val cont2cont_CF1L = thm "cont2cont_CF1L";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	35	val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	36	val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	37	val contlub_abstraction = thm "contlub_abstraction";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	38	val mono2mono_app = thm "mono2mono_app";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	39	val cont2contlub_app = thm "cont2contlub_app";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	40	val cont2cont_app = thm "cont2cont_app";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	41	val cont2cont_app2 = thm "cont2cont_app2";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	42	val cont_id = thm "cont_id";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	43	val cont_const = thm "cont_const";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	44	val cont2cont_app3 = thm "cont2cont_app3";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	45	val CfunI = thm "CfunI";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	46	val flatdom2monofun = thm "flatdom2monofun";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	47	val chfindom_monofun2cont = thm "chfindom_monofun2cont";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	48	val flatdom_strict2cont = thm "flatdom_strict2cont";

author	huffman
	Fri, 04 Mar 2005 23:12:36 +0100
changeset 15576	efb95d0d01f7
parent 15565	2454493bd77b
child 16204	5dd79d3f0105
permissions	-rw-r--r--