isabelle: src/HOL/Orderings.ML@b6be1d1b66c5 (annotated)

15524 2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	1	(* legacy ML bindings *)
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	2
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	3	val order_eq_refl = thm "order_eq_refl";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	4	val order_less_irrefl = thm "order_less_irrefl";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	5	val order_le_less = thm "order_le_less";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	6	val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	7	val order_less_imp_le = thm "order_less_imp_le";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	8	val order_less_not_sym = thm "order_less_not_sym";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	9	val order_less_asym = thm "order_less_asym";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	10	val order_less_trans = thm "order_less_trans";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	11	val order_le_less_trans = thm "order_le_less_trans";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	12	val order_less_le_trans = thm "order_less_le_trans";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	13	val order_less_imp_not_less = thm "order_less_imp_not_less";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	14	val order_less_imp_triv = thm "order_less_imp_triv";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	15	val order_less_imp_not_eq = thm "order_less_imp_not_eq";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	16	val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	17	val linorder_less_linear = thm "linorder_less_linear";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	18	val linorder_cases = thm "linorder_cases";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	19	val linorder_not_less = thm "linorder_not_less";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	20	val linorder_not_le = thm "linorder_not_le";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	21	val linorder_neq_iff = thm "linorder_neq_iff";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	22	val linorder_neqE = thm "linorder_neqE";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	23	val order_refl = thm "order_refl";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	24	val order_trans = thm "order_trans";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	25	val order_antisym = thm "order_antisym";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	26	val order_less_le = thm "order_less_le";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	27	val linorder_linear = thm "linorder_linear";
21216 1c8580913738 made locale partial_order compatible with axclass order; changed import order; consecutive changes haftmann parents: 15791 diff changeset	28	val mono_def = thm "mono_def";
1c8580913738 made locale partial_order compatible with axclass order; changed import order; consecutive changes haftmann parents: 15791 diff changeset	29	val monoI = thm "monoI";
1c8580913738 made locale partial_order compatible with axclass order; changed import order; consecutive changes haftmann parents: 15791 diff changeset	30	val monoD = thm "monoD";

author	haftmann
	Wed, 22 Nov 2006 10:20:15 +0100
changeset 21455	b6be1d1b66c5
parent 21216	1c8580913738
child 21619	dea0914773f7
permissions	-rw-r--r--