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

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1
15562 8455c9671494 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: 15576 diff changeset	4	val antisym_less_inverse = thm "antisym_less_inverse";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 15562 diff changeset	5	val antisym_less = thm "antisym_less";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	6	val bin_chainmax = thm "bin_chainmax";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	7	val bin_chain = thm "bin_chain";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 15562 diff changeset	8	val box_less = thm "box_less";
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	9	val chain_def = thm "chain_def";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	10	val chainE = thm "chainE";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	11	val chainI = thm "chainI";
17372 d73f67e90a95 add theorem chain_const huffman parents: 16922 diff changeset	12	val chain_const = thm "chain_const";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	13	val chain_mono3 = thm "chain_mono3";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	14	val chain_mono = thm "chain_mono";
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	15	val chain_shift = thm "chain_shift";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	16	val chain_tord = thm "chain_tord";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	17	val finite_chain_def = thm "finite_chain_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	18	val is_lubD1 = thm "is_lubD1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	19	val is_lub_def = thm "is_lub_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	20	val is_lubI = thm "is_lubI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	21	val is_lub_lub = thm "is_lub_lub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	22	val is_lub_range_shift = thm "is_lub_range_shift";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	23	val is_ub_def = thm "is_ub_def";
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	24	val is_ub_lub = thm "is_ub_lub";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	25	val is_ub_range_shift = thm "is_ub_range_shift";
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	26	val lub_bin_chain = thm "lub_bin_chain";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	27	val lub_chain_maxelem = thm "lub_chain_maxelem";
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	28	val lub_const = thm "lub_const";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	29	val lub_def = thm "lub_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	30	val lub_finch1 = thm "lub_finch1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	31	val lub_finch2 = thm "lub_finch2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	32	val lubI = thm "lubI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	33	val lub_singleton = thm "lub_singleton";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	34	val lub = thm "lub";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	35	val max_in_chain_def = thm "max_in_chain_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	36	val minimal2UU = thm "minimal2UU";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	37	val po_eq_conv = thm "po_eq_conv";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	38	val refl_less = thm "refl_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	39	val thelubI = thm "thelubI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	40	val tord_def = thm "tord_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	41	val trans_less = thm "trans_less";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	42	val ub_rangeD = thm "ub_rangeD";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	43	val ub_rangeI = thm "ub_rangeI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 15576 diff changeset	44	val unique_lub = thm "unique_lub";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45
15562 8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	46	structure Porder =
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	47	struct
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	48	val thy = the_context ();
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	49	val is_ub_def = is_ub_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	50	val is_lub_def = is_lub_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	51	val tord_def = tord_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	52	val chain_def = chain_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	53	val max_in_chain_def = max_in_chain_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	54	val finite_chain_def = finite_chain_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	55	val lub_def = lub_def;
8455c9671494 converted to new-style theory huffman parents: 14981 diff changeset	56	end;

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