isabelle: src/HOLCF/Pcpo.ML@0ee7eab8c845 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1
15563 9e125b675253 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: 15563 diff changeset	4	val ax_flat = thm "ax_flat";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	5	val ch2ch_lub = thm "ch2ch_lub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	6	val chain_mono2 = thm "chain_mono2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	7	val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	8	val chain_UU_I_inverse = thm "chain_UU_I_inverse";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	9	val chain_UU_I = thm "chain_UU_I";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	10	val chfin2finch = thm "chfin2finch";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	11	val chfin_imp_cpo = thm "chfin_imp_cpo";
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	12	val chfin = thm "chfin";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	13	val cpo = thm "cpo";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	14	val diag_lub = thm "diag_lub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	15	val eq_UU_iff = thm "eq_UU_iff";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	16	val ex_lub = thm "ex_lub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	17	val flat_eq = thm "flat_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	18	val flat_imp_chfin = thm "flat_imp_chfin";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	19	val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	20	val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	21	val is_lub_thelub = thm "is_lub_thelub";
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	22	val is_ub_thelub = thm "is_ub_thelub";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	23	val least = thm "least";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	24	val lub_equal2 = thm "lub_equal2";
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	25	val lub_equal = thm "lub_equal";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	26	val lub_mono2 = thm "lub_mono2";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	27	val lub_mono3 = thm "lub_mono3";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	28	val lub_mono = thm "lub_mono";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	29	val lub_range_shift = thm "lub_range_shift";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	30	val maxinch_is_thelub = thm "maxinch_is_thelub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	31	val minimal = thm "minimal";
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	32	val not_less2not_eq = thm "not_less2not_eq";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	33	val notUU_I = thm "notUU_I";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	34	val thelubE = thm "thelubE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	35	val UU_def = thm "UU_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	36	val UU_I = thm "UU_I";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	37	val UU_least = thm "UU_least";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15563 diff changeset	38	val UU_reorient = thm "UU_reorient";
3326 930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 3323 diff changeset	39
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	40	structure Pcpo =
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	41	struct
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	42	val thy = the_context ();
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	43	val UU_def = UU_def;
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	44	end;

author	nipkow
	Wed, 04 Jan 2006 16:38:40 +0100
changeset 18573	0ee7eab8c845
parent 16922	2128ac2aa5db
permissions	-rw-r--r--