--- a/src/HOL/Hyperreal/HyperOrd.thy Wed Jan 28 10:41:49 2004 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.thy Wed Jan 28 17:01:01 2004 +0100
@@ -7,10 +7,6 @@
theory HyperOrd = HyperDef:
-ML
-{*
-val left_distrib = thm"left_distrib";
-*}
(*** Monotonicity results ***)