isabelle: src/HOLCF/Pcpo.ML@d6156cb8dc2e (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
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	4	val cpo = thm "cpo";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	5	val least = thm "least";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	6	val UU_def = thm "UU_def";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	7	val chfin = thm "chfin";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	8	val ax_flat = thm "ax_flat";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	9	val UU_least = thm "UU_least";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	10	val minimal = thm "minimal";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	11	val thelubE = thm "thelubE";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	12	val is_ub_thelub = thm "is_ub_thelub";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	13	val is_lub_thelub = thm "is_lub_thelub";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	14	val lub_range_shift = thm "lub_range_shift";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	15	val maxinch_is_thelub = thm "maxinch_is_thelub";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	16	val lub_mono = thm "lub_mono";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	17	val lub_equal = thm "lub_equal";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	18	val lub_mono2 = thm "lub_mono2";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	19	val lub_equal2 = thm "lub_equal2";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	20	val lub_mono3 = thm "lub_mono3";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	21	val eq_UU_iff = thm "eq_UU_iff";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	22	val UU_I = thm "UU_I";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	23	val not_less2not_eq = thm "not_less2not_eq";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	24	val chain_UU_I = thm "chain_UU_I";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	25	val chain_UU_I_inverse = thm "chain_UU_I_inverse";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	26	val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	27	val notUU_I = thm "notUU_I";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	28	val chain_mono2 = thm "chain_mono2";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	29	val flat_imp_chfin = thm "flat_imp_chfin";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	30	val flat_eq = thm "flat_eq";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	31	val chfin2finch = thm "chfin2finch";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	32	val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	33	val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
3326 930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 3323 diff changeset	34
15563 9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	35	structure Pcpo =
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	36	struct
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	37	val thy = the_context ();
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	38	val UU_def = UU_def;
9e125b675253 converted to new-style theory huffman parents: 14981 diff changeset	39	end;

author	kleing
	Sat, 30 Apr 2005 14:18:36 +0200
changeset 15900	d6156cb8dc2e
parent 15563	9e125b675253
child 16922	2128ac2aa5db
permissions	-rw-r--r--