isabelle: src/HOLCF/Ssum.ML@278eb6251dc0 (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: 16752 diff changeset	4	val beta_sscase = thm "beta_sscase";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	5	val cont_Iwhen1 = thm "cont_Iwhen1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	6	val cont_Iwhen2 = thm "cont_Iwhen2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	7	val cont_Iwhen3 = thm "cont_Iwhen3";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	8	val Exh_Ssum = thm "Exh_Ssum";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	9	val Iwhen1 = thm "Iwhen1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	10	val Iwhen2 = thm "Iwhen2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	11	val Iwhen3 = thm "Iwhen3";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	12	val Iwhen4 = thm "Iwhen4";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	13	val Iwhen5 = thm "Iwhen5";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	14	val Iwhen_def = thm "Iwhen_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	15	val less_sinlD = thm "less_sinlD";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	16	val less_sinrD = thm "less_sinrD";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	17	val less_ssum_def = thm "less_Ssum_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	18	val Rep_Ssum_sinl = thm "Rep_Ssum_sinl";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	19	val Rep_Ssum_sinr = thm "Rep_Ssum_sinr";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	20	val sinl_Abs_Ssum = thm "sinl_Abs_Ssum";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	21	val sinl_defined_iff = thm "sinl_defined_iff";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	22	val sinl_defined = thm "sinl_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	23	val sinl_def = thm "sinl_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	24	val sinl_eq_sinr = thm "sinl_eq_sinr";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	25	val sinl_eq = thm "sinl_eq";
16211 faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas huffman parents: 16060 diff changeset	26	val sinl_inject = thm "sinl_inject";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	27	val sinl_less_sinr = thm "sinl_less_sinr";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	28	val sinl_less = thm "sinl_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	29	val sinl_strict = thm "sinl_strict";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	30	val sinr_Abs_Ssum = thm "sinr_Abs_Ssum";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	31	val sinr_defined_iff = thm "sinr_defined_iff";
16211 faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas huffman parents: 16060 diff changeset	32	val sinr_defined = thm "sinr_defined";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	33	val sinr_def = thm "sinr_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	34	val sinr_eq_sinl = thm "sinr_eq_sinl";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	35	val sinr_eq = thm "sinr_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	36	val sinr_inject = thm "sinr_inject";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	37	val sinr_less_sinl = thm "sinr_less_sinl";
16316 17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names huffman parents: 16211 diff changeset	38	val sinr_less = thm "sinr_less";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	39	val sinr_strict = thm "sinr_strict";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	40	val sscase1 = thm "sscase1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	41	val sscase2 = thm "sscase2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	42	val sscase3 = thm "sscase3";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43	val sscase4 = thm "sscase4";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	44	val sscase_def = thm "sscase_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	45	val ssum_chain_lemma = thm "ssum_chain_lemma";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	46	val ssumE2 = thm "ssumE2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16752 diff changeset	47	val ssumE = thm "ssumE";
16211 faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas huffman parents: 16060 diff changeset	48	val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas huffman parents: 16060 diff changeset	49	sscase1, sscase2, sscase3];

author	paulson
	Thu, 18 Aug 2005 13:09:40 +0200
changeset 17122	278eb6251dc0
parent 16922	2128ac2aa5db
child 17838	3032e90c4975
permissions	-rw-r--r--