--- a/src/HOL/NSA/HyperDef.thy Thu Mar 20 09:47:43 2014 +0100
+++ b/src/HOL/NSA/HyperDef.thy Thu Mar 20 12:43:48 2014 +0000
@@ -225,14 +225,6 @@
"abs (star_n X) = star_n (%n. abs (X n))"
by (simp only: star_abs_def starfun_star_n)
-subsection{*Misc Others*}
-
-lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
-by (auto)
-
-lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
-by auto
-
lemma hypreal_omega_gt_zero [simp]: "0 < omega"
by (simp add: omega_def star_n_zero_num star_n_less)