# HG changeset patch
# User wenzelm
# Date 1165363971 -3600
# Node ID a664ba87b3aa283c3fa7837857ff1b59796769fa
# Parent  29c346b165d44ddeb25a95098efa058f80df5e49
added basic ML bindings;

diff -r 29c346b165d4 -r a664ba87b3aa src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Dec 06 01:12:43 2006 +0100
+++ b/src/HOL/Orderings.thy	Wed Dec 06 01:12:51 2006 +0100
@@ -909,4 +909,31 @@
     "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   by (simp add: max_def)
 
+
+subsection {* Basic ML bindings *}
+
+ML {*
+val leD = thm "leD";
+val leI = thm "leI";
+val linorder_neqE = thm "linorder_neqE";
+val linorder_neq_iff = thm "linorder_neq_iff";
+val linorder_not_le = thm "linorder_not_le";
+val linorder_not_less = thm "linorder_not_less";
+val monoD = thm "monoD";
+val monoI = thm "monoI";
+val order_antisym = thm "order_antisym";
+val order_less_irrefl = thm "order_less_irrefl";
+val order_refl = thm "order_refl";
+val order_trans = thm "order_trans";
+val split_max = thm "split_max";
+val split_min = thm "split_min";
+*}
+
+ML {*
+structure HOL =
+struct
+  val thy = theory "HOL";
+end;
+*}  -- "belongs to theory HOL"
+
 end