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

author	huffman
	Wed, 02 Mar 2005 22:30:00 +0100
changeset 15562	8455c9671494
parent 14981	e73f8140af78
child 15576	efb95d0d01f7
permissions	-rw-r--r--