isabelle: src/HOLCF/Sprod.ML@04c2c702a3fb (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
17838 3032e90c4975 added compactness theorems huffman parents: 16923 diff changeset	4	val compact_spair = thm "compact_spair";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	5	val eq_sprod = thm "eq_sprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	6	val Exh_Sprod2 = thm "Exh_Sprod2"; (* *)
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	7	val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *)
16699 24b494ff8f0f use new pcpodef package huffman parents: 16317 diff changeset	8	val less_sprod_def = thm "less_Sprod_def";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	9	val less_sprod = thm "less_sprod";
16923 2d9ebdc0c1ee fixed typo huffman parents: 16922 diff changeset	10	val Rep_Sprod_spair = thm "Rep_Sprod_spair";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	11	val sfst_defined_iff = thm "sfst_defined_iff";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	12	val sfst_defined = thm "sfst_defined";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	13	val sfst_def = thm "sfst_def";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	14	val sfst_spair = thm "sfst_spair";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	15	val sfst_strict = thm "sfst_strict";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	16	val spair_Abs_Sprod = thm "spair_Abs_Sprod";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	17	val spair_defined_rev = thm "spair_defined_rev";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	18	val spair_defined = thm "spair_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	19	val spair_def = thm "spair_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	20	val spair_eq = thm "spair_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	21	val spair_inject = thm "spair_inject";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	22	val spair_lemma = thm "spair_lemma";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	23	val spair_less = thm "spair_less";
16212 422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair huffman parents: 16059 diff changeset	24	val spair_strict1 = thm "spair_strict1";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair huffman parents: 16059 diff changeset	25	val spair_strict2 = thm "spair_strict2";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair huffman parents: 16059 diff changeset	26	val spair_strict_rev = thm "spair_strict_rev";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	27	val spair_strict = thm "spair_strict";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	28	val sprodE = thm "sprodE";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	29	val ssnd_defined_iff = thm "ssnd_defined_iff";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	30	val ssnd_defined = thm "ssnd_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	31	val ssnd_def = thm "ssnd_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	32	val ssnd_spair = thm "ssnd_spair";
16212 422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair huffman parents: 16059 diff changeset	33	val ssnd_strict = thm "ssnd_strict";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	34	val ssplit1 = thm "ssplit1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	35	val ssplit2 = thm "ssplit2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	36	val ssplit3 = thm "ssplit3";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	37	val ssplit_def = thm "ssplit_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16777 diff changeset	38	val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";

author	wenzelm
	Sat, 07 Jan 2006 12:26:27 +0100
changeset 18603	04c2c702a3fb
parent 17838	3032e90c4975
permissions	-rw-r--r--