isabelle: src/HOLCF/Up.ML@3b643f81b378 (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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	4	val antisym_less_up = thm "antisym_less_up";
17838 3032e90c4975 added compactness theorems huffman parents: 16922 diff changeset	5	val compact_up = thm "compact_up";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	6	val cont_Ifup1 = thm "cont_Ifup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	7	val cont_Ifup2 = thm "cont_Ifup2";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	8	val cont_Iup = thm "cont_Iup";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	9	val cpo_up = thm "cpo_up";
16753 fb6801c926d2 define 'a u with datatype package; huffman parents: 16319 diff changeset	10	val Exh_Up = thm "Exh_Up";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	11	val fup1 = thm "fup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	12	val fup2 = thm "fup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	13	val fup3 = thm "fup3";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	14	val fup_def = thm "fup_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	15	val inst_up_pcpo = thm "inst_up_pcpo";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	16	val is_lub_Iup = thm "is_lub_Iup";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	17	val Iup_less = thm "Iup_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	18	val least_up = thm "least_up";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	19	val less_up_def = thm "less_up_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	20	val minimal_up = thm "minimal_up";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	21	val monofun_Ifup2 = thm "monofun_Ifup2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	22	val not_Iup_less = thm "not_Iup_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	23	val not_up_less_UU = thm "not_up_less_UU";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	24	val refl_less_up = thm "refl_less_up";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	25	val trans_less_up = thm "trans_less_up";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	26	val up_chain_cases = thm "up_chain_cases";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	27	val up_defined = thm "up_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	28	val up_def = thm "up_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	29	val up_eq = thm "up_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	30	val upE = thm "upE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	31	val up_inject = thm "up_inject";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	32	val up_lemma1 = thm "up_lemma1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	33	val up_lemma2 = thm "up_lemma2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	34	val up_lemma3 = thm "up_lemma3";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	35	val up_lemma4 = thm "up_lemma4";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	36	val up_lemma5 = thm "up_lemma5";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	37	val up_lemma6 = thm "up_lemma6";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	38	val up_less = thm "up_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16753 diff changeset	39

author	wenzelm
	Wed, 01 Feb 2006 22:20:40 +0100
changeset 18888	3b643f81b378
parent 17838	3032e90c4975
permissions	-rw-r--r--