isabelle: src/HOLCF/Cfun.ML@3eb21fb8c2ec (annotated)

15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	2	(* legacy ML bindings *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	3
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	4	val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	5	val adm_cont = thm "adm_cont";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	6	val assoc_oo = thm "assoc_oo";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	7	val beta_cfun = thm "beta_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	8	val cfcomp1 = thm "cfcomp1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	9	val cfcomp2 = thm "cfcomp2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	10	val cfun_arg_cong = thm "cfun_arg_cong";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	11	val cfun_cong = thm "cfun_cong";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	12	val cfun_fun_cong = thm "cfun_fun_cong";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	13	val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	14	val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	15	val ch2ch_Rep_CFun = thm "ch2ch_Rep_CFun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	16	val chain_monofun = thm "chain_monofun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	17	val chfin2chfin = thm "chfin2chfin";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	18	val chfin_Rep_CFunR = thm "chfin_Rep_CFunR";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	19	val cont2cont_LAM = thm "cont2cont_LAM";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	20	val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	21	val cont2mono_LAM = thm "cont2mono_LAM";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	22	val cont_cfun_arg = thm "cont_cfun_arg";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	23	val cont_cfun_fun = thm "cont_cfun_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	24	val cont_cfun = thm "cont_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	25	val cont_Istrictify1 = thm "cont_Istrictify1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	26	val cont_Istrictify2 = thm "cont_Istrictify2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	27	val cont_lemmas1 = thms "cont_lemmas1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	28	val contlub_cfun_arg = thm "contlub_cfun_arg";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	29	val contlub_cfun_fun = thm "contlub_cfun_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	30	val cont_lub_cfun = thm "cont_lub_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	31	val contlub_cfun = thm "contlub_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	32	val contlub_Istrictify2 = thm "contlub_Istrictify2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	33	val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	34	val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	35	val cont_Rep_CFun1 = thm "cont_Rep_CFun1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	36	val cont_Rep_CFun2 = thm "cont_Rep_CFun2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	37	val eta_cfun = thm "eta_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	38	val ex_lub_cfun = thm "ex_lub_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	39	val ext_cfun = thm "ext_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	40	val flat2flat = thm "flat2flat";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	41	val flat_codom = thm "flat_codom";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	42	val flat_eqI = thm "flat_eqI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	43	val ID1 = thm "ID1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	44	val ID2 = thm "ID2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	45	val ID3 = thm "ID3";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	46	val ID_def = thm "ID_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	47	val injection_defined_rev = thm "injection_defined_rev";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	48	val injection_defined = thm "injection_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	49	val injection_eq = thm "injection_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	50	val injection_less = thm "injection_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	51	val inst_cfun_pcpo = thm "inst_cfun_pcpo";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	52	val Istrictify1 = thm "Istrictify1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	53	val Istrictify2 = thm "Istrictify2";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	54	val Istrictify_def = thm "Istrictify_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	55	val less_cfun_def = thm "less_CFun_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	56	val less_cfun_ext = thm "less_cfun_ext";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	57	val lub_cfun_mono = thm "lub_cfun_mono";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	58	val lub_cfun = thm "lub_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	59	val monofun_cfun_arg = thm "monofun_cfun_arg";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	60	val monofun_cfun_fun = thm "monofun_cfun_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	61	val monofun_cfun = thm "monofun_cfun";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	62	val monofun_Istrictify2 = thm "monofun_Istrictify2";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	63	val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	64	val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	65	val oo_def = thm "oo_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	66	val Rep_CFun_strict1 = thm "Rep_CFun_strict1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	67	val retraction_strict = thm "retraction_strict";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	68	val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	69	val strictify1 = thm "strictify1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	70	val strictify2 = thm "strictify2";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	71	val strictify_conv_if = thm "strictify_conv_if";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	72	val strictify_def = thm "strictify_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	73	val strictI = thm "strictI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	74	val thelub_cfun = thm "thelub_cfun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16699 diff changeset	75	val UU_CFun = thm "UU_CFun";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	76
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	77	structure Cfun =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	78	struct
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	79	val thy = the_context ();
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	80	val Istrictify_def = Istrictify_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	81	val strictify_def = strictify_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	82	val ID_def = ID_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	83	val oo_def = oo_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	84	end;

author	wenzelm
	Wed, 14 Sep 2005 22:04:34 +0200
changeset 17383	3eb21fb8c2ec
parent 16922	2128ac2aa5db
child 17815	ccf54e3cabfa
permissions	-rw-r--r--