isabelle: src/HOLCF/Cont.ML@dc1d6f588204 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1
15565 2454493bd77b 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
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	4	val binchain_cont = thm "binchain_cont";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	5	val ch2ch_cont = thm "ch2ch_cont";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	6	val ch2ch_monofun = thm "ch2ch_monofun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	7	val chfindom_monofun2cont = thm "chfindom_monofun2cont";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	8	val cont2cont_app2 = thm "cont2cont_app2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	9	val cont2cont_app3 = thm "cont2cont_app3";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	10	val cont2cont_app = thm "cont2cont_app";
18092 2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM huffman parents: 16922 diff changeset	11	val cont2cont_fun = thm "cont2cont_fun";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	12	val cont2cont_lambda = thm "cont2cont_lambda";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	13	val cont2contlub_app = thm "cont2contlub_app";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	14	val cont2contlubE = thm "cont2contlubE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	15	val cont2cont_lub = thm "cont2cont_lub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	16	val cont2contlub = thm "cont2contlub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	17	val cont2mono = thm "cont2mono";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	18	val cont_const = thm "cont_const";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	19	val cont_def = thm "cont_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	20	val contE = thm "contE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	21	val cont_finch2finch = thm "cont_finch2finch";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	22	val cont_id = thm "cont_id";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	23	val cont_if = thm "cont_if";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	24	val contI = thm "contI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	25	val contlub_abstraction = thm "contlub_abstraction";
16204 5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs. huffman parents: 15565 diff changeset	26	val contlub_def = thm "contlub_def";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	27	val contlubE = thm "contlubE";
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	28	val contlubI = thm "contlubI";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	29	val contlub_lub_fun = thm "contlub_lub_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	30	val flatdom_strict2cont = thm "flatdom_strict2cont";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	31	val flatdom_strict2mono = thm "flatdom_strict2mono";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	32	val mono2mono_app = thm "mono2mono_app";
18092 2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM huffman parents: 16922 diff changeset	33	val mono2mono_fun = thm "mono2mono_fun";
2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM huffman parents: 16922 diff changeset	34	val mono2mono_lambda = thm "mono2mono_lambda";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	35	val monocontlub2cont = thm "monocontlub2cont";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	36	val monofun_def = thm "monofun_def";
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	37	val monofunE = thm "monofunE";
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	38	val monofun_finch2finch = thm "monofun_finch2finch";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	39	val monofun_fun_arg = thm "monofun_fun_arg";
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	40	val monofun_fun_fun = thm "monofun_fun_fun";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	41	val monofun_fun = thm "monofun_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	42	val monofunI = thm "monofunI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	43	val monofun_lub_fun = thm "monofun_lub_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16625 diff changeset	44	val ub2ub_monofun = thm "ub2ub_monofun";

author	huffman
	Mon, 07 Nov 2005 23:33:01 +0100
changeset 18112	dc1d6f588204
parent 18092	2c5d5da79a1e
permissions	-rw-r--r--