isabelle: src/HOL/HOL.ML@a3519c0c2d8f (annotated)

21670 704510b508ef reduced to genuine legacy bindings -- others in HOL.thy; wenzelm parents: 21619 diff changeset	1	(*
704510b508ef reduced to genuine legacy bindings -- others in HOL.thy; wenzelm parents: 21619 diff changeset	2	ID: $Id$
704510b508ef reduced to genuine legacy bindings -- others in HOL.thy; wenzelm parents: 21619 diff changeset	3	*)
21546 268b6bed0cc8 removed HOL structure haftmann parents: 21379 diff changeset	4
21670 704510b508ef reduced to genuine legacy bindings -- others in HOL.thy; wenzelm parents: 21619 diff changeset	5	( legacy ML bindings )
12999 8ad8d02b973f tuned; wenzelm parents: 11977 diff changeset	6
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	7	val all_conj_distrib = thm "all_conj_distrib";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	8	val all_simps = thms "all_simps";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	9	val atomize_not = thm "atomize_not";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	10	val case_split = thm "case_split_thm";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	11	val case_split_thm = thm "case_split_thm"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	12	val cases_simp = thm "cases_simp";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	13	val choice_eq = thm "choice_eq"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	14	val cong = thm "cong"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	15	val conj_comms = thms "conj_comms";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	16	val conj_cong = thm "conj_cong";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	17	val def_imp_eq = thm "def_imp_eq";
20944 34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	18	val de_Morgan_conj = thm "de_Morgan_conj";
34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	19	val de_Morgan_disj = thm "de_Morgan_disj";
34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	20	val disj_assoc = thm "disj_assoc";
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	21	val disj_comms = thms "disj_comms";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	22	val disj_cong = thm "disj_cong";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	23	val eq_ac = thms "eq_ac";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	24	val eq_cong2 = thm "eq_cong2"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	25	val Eq_FalseI = thm "Eq_FalseI";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	26	val Eq_TrueI = thm "Eq_TrueI";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	27	val Ex1_def = thm "Ex1_def"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	28	val ex_disj_distrib = thm "ex_disj_distrib";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	29	val ex_simps = thms "ex_simps";
20944 34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	30	val if_cancel = thm "if_cancel";
34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	31	val if_eq_cancel = thm "if_eq_cancel";
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	32	val if_False = thm "if_False";
20944 34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	33	val iff_conv_conj_imp = thm "iff_conv_conj_imp";
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	34	val iff = thm "iff"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	35	val if_splits = thms "if_splits";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	36	val if_True = thm "if_True";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	37	val if_weak_cong = thm "if_weak_cong"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	38	val imp_all = thm "imp_all";
20944 34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	39	val imp_cong = thm "imp_cong";
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	40	val imp_conjL = thm "imp_conjL";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	41	val imp_conjR = thm "imp_conjR";
20944 34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	42	val imp_conv_disj = thm "imp_conv_disj";
34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	43	val simp_implies_def = thm "simp_implies_def";
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	44	val simp_thms = thms "simp_thms";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	45	val split_if = thm "split_if";
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	46	val the1_equality = thm "the1_equality"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	47	val theI = thm "theI"
dea0914773f7 stripped some legacy bindings haftmann parents: 21546 diff changeset	48	val theI' = thm "theI'"
20944 34b2c1bb7178 cleanup basic HOL bootstrap haftmann parents: 18916 diff changeset	49	val True_implies_equals = thm "True_implies_equals";

author	wenzelm
	Fri, 05 Jan 2007 14:30:07 +0100
changeset 22013	a3519c0c2d8f
parent 21670	704510b508ef
child 22218	30a8890d2967
permissions	-rw-r--r--