isabelle: src/HOLCF/Ssum3.ML@41bfe19eabe2 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1
15568 41bfe19eabe2 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
15568 41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	4	val sinl_def = thm "sinl_def";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	5	val sinr_def = thm "sinr_def";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	6	val sscase_def = thm "sscase_def";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	7	val inst_ssum_pcpo = thm "inst_ssum_pcpo";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	8	val contlub_Isinl = thm "contlub_Isinl";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	9	val contlub_Isinr = thm "contlub_Isinr";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	10	val cont_Isinl = thm "cont_Isinl";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	11	val cont_Isinr = thm "cont_Isinr";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	12	val contlub_Iwhen1 = thm "contlub_Iwhen1";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	13	val contlub_Iwhen2 = thm "contlub_Iwhen2";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	14	val ssum_lemma9 = thm "ssum_lemma9";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	15	val ssum_lemma10 = thm "ssum_lemma10";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	16	val ssum_lemma11 = thm "ssum_lemma11";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	17	val ssum_lemma12 = thm "ssum_lemma12";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	18	val ssum_lemma13 = thm "ssum_lemma13";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	19	val contlub_Iwhen3 = thm "contlub_Iwhen3";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	20	val cont_Iwhen1 = thm "cont_Iwhen1";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	21	val cont_Iwhen2 = thm "cont_Iwhen2";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	22	val cont_Iwhen3 = thm "cont_Iwhen3";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	23	val strict_sinl = thm "strict_sinl";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	24	val strict_sinr = thm "strict_sinr";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	25	val noteq_sinlsinr = thm "noteq_sinlsinr";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	26	val inject_sinl = thm "inject_sinl";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	27	val inject_sinr = thm "inject_sinr";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	28	val defined_sinl = thm "defined_sinl";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	29	val defined_sinr = thm "defined_sinr";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	30	val Exh_Ssum1 = thm "Exh_Ssum1";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	31	val ssumE = thm "ssumE";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	32	val ssumE2 = thm "ssumE2";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	33	val sscase1 = thm "sscase1";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	34	val sscase2 = thm "sscase2";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	35	val sscase3 = thm "sscase3";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	36	val less_ssum4a = thm "less_ssum4a";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	37	val less_ssum4b = thm "less_ssum4b";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	38	val less_ssum4c = thm "less_ssum4c";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	39	val less_ssum4d = thm "less_ssum4d";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	40	val ssum_chainE = thm "ssum_chainE";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	41	val thelub_ssum2a = thm "thelub_ssum2a";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	42	val thelub_ssum2b = thm "thelub_ssum2b";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	43	val thelub_ssum2a_rev = thm "thelub_ssum2a_rev";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	44	val thelub_ssum2b_rev = thm "thelub_ssum2b_rev";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	45	val thelub_ssum3 = thm "thelub_ssum3";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	46	val sscase4 = thm "sscase4";
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	47	val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr,
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	48	sscase1, sscase2, sscase3]

author	huffman
	Thu, 03 Mar 2005 01:37:32 +0100
changeset 15568	41bfe19eabe2
parent 14981	e73f8140af78
permissions	-rw-r--r--