isabelle: src/HOL/Orderings.ML@dea0914773f7 (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_less_irrefl = thm "order_less_irrefl";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	4	val linorder_not_less = thm "linorder_not_less";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	5	val linorder_not_le = thm "linorder_not_le";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	6	val linorder_neq_iff = thm "linorder_neq_iff";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	7	val linorder_neqE = thm "linorder_neqE";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	8	val order_refl = thm "order_refl";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	9	val order_trans = thm "order_trans";
2ef571f80a55 Moved oderings from HOL into the new Orderings.thy nipkow parents: diff changeset	10	val order_antisym = thm "order_antisym";
21216 1c8580913738 made locale partial_order compatible with axclass order; changed import order; consecutive changes haftmann parents: 15791 diff changeset	11	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	12	val monoI = thm "monoI";
1c8580913738 made locale partial_order compatible with axclass order; changed import order; consecutive changes haftmann parents: 15791 diff changeset	13	val monoD = thm "monoD";
21619 dea0914773f7 stripped some legacy bindings haftmann parents: 21216 diff changeset	14	val max_less_iff_conj = thm "max_less_iff_conj";
dea0914773f7 stripped some legacy bindings haftmann parents: 21216 diff changeset	15	val min_less_iff_conj = thm "min_less_iff_conj";
dea0914773f7 stripped some legacy bindings haftmann parents: 21216 diff changeset	16	val split_min = thm "split_min";
dea0914773f7 stripped some legacy bindings haftmann parents: 21216 diff changeset	17	val split_max = thm "split_max";

author	haftmann
	Fri, 01 Dec 2006 17:22:28 +0100
changeset 21619	dea0914773f7
parent 21216	1c8580913738
permissions	-rw-r--r--