isabelle: src/HOLCF/Lift.ML@e135f6a1b76c (annotated)

3655 0531f2c64c91 new extended adm tactic introduced; mueller parents: 3457 diff changeset	1
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	2	(* legacy ML bindings *)
3324 6b26b886ff69 Eliminated the prediates flat,chfin slotosch parents: diff changeset	3
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	4	structure lift =
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	5	struct
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	6	val distinct = thms "lift.distinct";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	7	val inject = thms "lift.inject";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	8	val exhaust = thm "lift.exhaust";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	9	val cases = thms "lift.cases";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	10	val split = thm "lift.split";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	11	val split_asm = thm "lift.split_asm";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	12	val induct = thm "lift.induct";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	13	val recs = thms "lift.recs";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	14	val simps = thms "lift.simps";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	15	val size = thms "lift.size";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	16	end;
3324 6b26b886ff69 Eliminated the prediates flat,chfin slotosch parents: diff changeset	17
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	18	val cont2cont_flift1 = thm "cont2cont_flift1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	19	val cont2cont_lift_case = thm "cont2cont_lift_case";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	20	val cont_flift1 = thm "cont_flift1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	21	val cont_lemmas_ext = thms "cont_lemmas_ext";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	22	val cont_lift_case1 = thm "cont_lift_case1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	23	val cont_lift_case2 = thm "cont_lift_case2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	24	val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	25	val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	26	val DefE2 = thm "DefE2";
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	27	val DefE = thm "DefE";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	28	val Def_inject_less_eq = thm "Def_inject_less_eq";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	29	val Def_inject = thm "Def_inject";
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	30	val Def_less_is_eq = thm "Def_less_is_eq";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	31	val Def_not_UU = thm "Def_not_UU";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	32	val flift1_def = thm "flift1_def";
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	33	val flift1_Def = thm "flift1_Def";
16695 dc8c868e910b simplified definitions of flift1, flift2, liftpair; huffman parents: 16388 diff changeset	34	val flift1_strict = thm "flift1_strict";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	35	val flift2_defined = thm "flift2_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	36	val flift2_def = thm "flift2_def";
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	37	val flift2_Def = thm "flift2_Def";
16695 dc8c868e910b simplified definitions of flift1, flift2, liftpair; huffman parents: 16388 diff changeset	38	val flift2_strict = thm "flift2_strict";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	39	val inst_lift_pcpo = thm "inst_lift_pcpo";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	40	val less_lift_def = thm "less_lift_def";
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	41	val less_lift = thm "less_lift";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	42	val Lift_cases = thm "Lift_cases";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	43	val lift_definedE = thm "lift_definedE";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	44	val lift_distinct1 = thm "lift_distinct1";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	45	val lift_distinct2 = thm "lift_distinct2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	46	val Lift_exhaust = thm "Lift_exhaust";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16757 diff changeset	47	val lift_induct = thm "lift_induct";
12026 0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	48	val liftpair_def = thm "liftpair_def";
0b1d80ada4ab rep_datatype lift; wenzelm parents: 10834 diff changeset	49	val not_Undef_is_Def = thm "not_Undef_is_Def";

author	wenzelm
	Tue, 10 Jan 2006 19:33:37 +0100
changeset 18638	e135f6a1b76c
parent 16922	2128ac2aa5db
permissions	-rw-r--r--