isabelle: src/HOLCF/Cfun3.ML@eb3b1a5c304e (annotated)

9245 428385c4bc50 removed most batch-style proofs paulson parents: 8820 diff changeset	1
15566 eb3b1a5c304e 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
15566 eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	4	val Istrictify_def = thm "Istrictify_def";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	5	val strictify_def = thm "strictify_def";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	6	val ID_def = thm "ID_def";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	7	val oo_def = thm "oo_def";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	8	val inst_cfun_pcpo = thm "inst_cfun_pcpo";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	9	val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	10	val cont_Rep_CFun1 = thm "cont_Rep_CFun1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	11	val contlub_cfun_fun = thm "contlub_cfun_fun";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	12	val cont_cfun_fun = thm "cont_cfun_fun";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	13	val contlub_cfun = thm "contlub_cfun";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	14	val cont_cfun = thm "cont_cfun";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	15	val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	16	val cont2mono_LAM = thm "cont2mono_LAM";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	17	val cont2cont_LAM = thm "cont2cont_LAM";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	18	val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	19	cont2cont_Rep_CFun, cont2cont_LAM];
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	20	val strict_Rep_CFun1 = thm "strict_Rep_CFun1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	21	val Istrictify1 = thm "Istrictify1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	22	val Istrictify2 = thm "Istrictify2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	23	val monofun_Istrictify1 = thm "monofun_Istrictify1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	24	val monofun_Istrictify2 = thm "monofun_Istrictify2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	25	val contlub_Istrictify1 = thm "contlub_Istrictify1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	26	val contlub_Istrictify2 = thm "contlub_Istrictify2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	27	val cont_Istrictify1 = thm "cont_Istrictify1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	28	val cont_Istrictify2 = thm "cont_Istrictify2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	29	val strictify1 = thm "strictify1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	30	val strictify2 = thm "strictify2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	31	val chfin_Rep_CFunR = thm "chfin_Rep_CFunR";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	32	val iso_strict = thm "iso_strict";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	33	val isorep_defined = thm "isorep_defined";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	34	val isoabs_defined = thm "isoabs_defined";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	35	val chfin2chfin = thm "chfin2chfin";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	36	val flat2flat = thm "flat2flat";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	37	val flat_codom = thm "flat_codom";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	38	val ID1 = thm "ID1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	39	val cfcomp1 = thm "cfcomp1";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	40	val cfcomp2 = thm "cfcomp2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	41	val ID2 = thm "ID2";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	42	val ID3 = thm "ID3";
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	43	val assoc_oo = thm "assoc_oo";
3326 930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo. slotosch parents: 3031 diff changeset	44
15566 eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	45	structure Cfun3 =
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	46	struct
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	47	val thy = the_context ();
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	48	val Istrictify_def = Istrictify_def;
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	49	val strictify_def = strictify_def;
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	50	val ID_def = ID_def;
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	51	val oo_def = oo_def;
eb3b1a5c304e converted to new-style theory huffman parents: 14981 diff changeset	52	end;

author	huffman
	Wed, 02 Mar 2005 23:58:02 +0100
changeset 15566	eb3b1a5c304e
parent 14981	e73f8140af78
permissions	-rw-r--r--