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

author	quigley
	Mon, 23 May 2005 15:16:36 +0200
changeset 16048	25cb0fe2e1c6
parent 15576	efb95d0d01f7
child 16922	2128ac2aa5db
permissions	-rw-r--r--