isabelle: src/HOLCF/Cprod.ML@3b643f81b378 (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: 16210 diff changeset	4	val antisym_less_cprod = thm "antisym_less_cprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	5	val cfst_cpair = thm "cfst_cpair";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	6	val cfst_def = thm "cfst_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	7	val cfst_strict = thm "cfst_strict";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	8	val CLet_def = thm "CLet_def";
17838 3032e90c4975 added compactness theorems huffman parents: 16922 diff changeset	9	val compact_cpair = thm "compact_cpair";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	10	val cont_fst = thm "cont_fst";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	11	val contlub_fst = thm "contlub_fst";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	12	val contlub_pair1 = thm "contlub_pair1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	13	val contlub_pair2 = thm "contlub_pair2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	14	val contlub_snd = thm "contlub_snd";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	15	val cont_pair1 = thm "cont_pair1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	16	val cont_pair2 = thm "cont_pair2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	17	val cont_snd = thm "cont_snd";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	18	val cpair_def = thm "cpair_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	19	val cpair_defined_iff = thm "cpair_defined_iff";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	20	val cpair_eq_pair = thm "cpair_eq_pair";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	21	val cpair_eq = thm "cpair_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	22	val cpair_less = thm "cpair_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	23	val cpo_cprod = thm "cpo_cprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	24	val cprodE = thm "cprodE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	25	val Cprod_rews = thms "Cprod_rews";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	26	val csnd_cpair = thm "csnd_cpair";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	27	val csnd_def = thm "csnd_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	28	val csnd_strict = thm "csnd_strict";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	29	val csplit2 = thm "csplit2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	30	val csplit3 = thm "csplit3";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	31	val csplit_def = thm "csplit_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	32	val defined_cpair_rev = thm "defined_cpair_rev";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	33	val eq_cprod = thm "eq_cprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	34	val Exh_Cprod2 = thm "Exh_Cprod2"; (* rename *)
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	35	val inject_cpair = thm "inject_cpair";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	36	val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; (**)
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	37	val inst_cprod_pcpo = thm "inst_cprod_pcpo";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	38	val least_cprod = thm "least_cprod";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	39	val less_cprod_def = thm "less_cprod_def";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	40	val less_cprod = thm "less_cprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	41	val lub_cprod2 = thm "lub_cprod2"; (* *)
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	42	val lub_cprod = thm "lub_cprod";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43	val minimal_cprod = thm "minimal_cprod";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	44	val monofun_fst = thm "monofun_fst";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	45	val monofun_pair1 = thm "monofun_pair1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	46	val monofun_pair2 = thm "monofun_pair2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	47	val monofun_pair = thm "monofun_pair";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	48	val monofun_snd = thm "monofun_snd";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	49	val refl_less_cprod = thm "refl_less_cprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	50	val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; (* rename *)
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	51	val thelub_cprod2 = thm "thelub_cprod2"; (* *)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	52	val thelub_cprod = thm "thelub_cprod";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16210 diff changeset	53	val trans_less_cprod = thm "trans_less_cprod";

author	wenzelm
	Wed, 01 Feb 2006 22:20:40 +0100
changeset 18888	3b643f81b378
parent 17838	3032e90c4975
permissions	-rw-r--r--