isabelle: src/HOLCF/Tr.ML@d73f67e90a95 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	1
15649 f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	2	(* legacy ML bindings *)
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	3
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	4	val adm_nFF = thm "adm_nFF";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	5	val adm_nTT = thm "adm_nTT";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	6	val adm_trick_1 = thm "adm_trick_1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	7	val adm_trick_2 = thm "adm_trick_2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	8	val adm_tricks = thms "adm_tricks";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	9	val andalso_and = thm "andalso_and";
15649 f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	10	val andalso_def = thm "andalso_def";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	11	val andalso_or = thm "andalso_or";
15649 f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	12	val andalso_thms = thms "andalso_thms";
f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	13	val Def_bool1 = thm "Def_bool1";
f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	14	val Def_bool2 = thm "Def_bool2";
f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	15	val Def_bool3 = thm "Def_bool3";
f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	16	val Def_bool4 = thm "Def_bool4";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	17	val dist_eq_tr = thms "dist_eq_tr";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	18	val dist_less_tr = thms "dist_less_tr";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	19	val Exh_tr = thm "Exh_tr";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	20	val FF_def = thm "FF_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	21	val If2_def = thm "If2_def";
15649 f8345ee4f607 convert to new-style theory huffman parents: 14981 diff changeset	22	val If_and_if = thm "If_and_if";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	23	val ifte_def = thm "ifte_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	24	val ifte_thms = thms "ifte_thms";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	25	val neg_def = thm "neg_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	26	val neg_thms = thms "neg_thms";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	27	val orelse_def = thm "orelse_def";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	28	val orelse_thms = thms "orelse_thms";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	29	val split_If2 = thm "split_If2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	30	val tr_defs = thms "tr_defs";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	31	val trE = thm "trE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16756 diff changeset	32	val TT_def = thm "TT_def";

author	huffman
	Tue, 13 Sep 2005 23:30:01 +0200
changeset 17372	d73f67e90a95
parent 16922	2128ac2aa5db
child 18070	b653e18f0a41
permissions	-rw-r--r--