isabelle: src/HOLCF/Ffun.ML@3b643f81b378 (annotated)

16202 61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	1
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	2	(* legacy ML bindings *)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	3
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	4	val antisym_less_fun = thm "antisym_less_fun";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	5	val app_strict = thm "app_strict";
16202 61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	6	val ch2ch_fun = thm "ch2ch_fun";
18092 2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM huffman parents: 17831 diff changeset	7	val ch2ch_lambda = thm "ch2ch_lambda";
16202 61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	8	val cpo_fun = thm "cpo_fun";
17831 4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less huffman parents: 16922 diff changeset	9	val expand_fun_less = thm "expand_fun_less";
16202 61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict huffman parents: diff changeset	10	val inst_fun_pcpo = thm "inst_fun_pcpo";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	11	val least_fun = thm "least_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	12	val less_fun_def = thm "less_fun_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	13	val less_fun_ext = thm "less_fun_ext";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	14	val lub_fun = thm "lub_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	15	val minimal_fun = thm "minimal_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	16	val refl_less_fun = thm "refl_less_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	17	val thelub_fun = thm "thelub_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	18	val trans_less_fun = thm "trans_less_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	19	val ub2ub_fun = thm "ub2ub_fun";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16202 diff changeset	20

author	wenzelm
	Wed, 01 Feb 2006 22:20:40 +0100
changeset 18888	3b643f81b378
parent 18092	2c5d5da79a1e
permissions	-rw-r--r--