src/HOL/Nonstandard_Analysis/HLog.thy

 section \<open>Logarithms: Non-Standard Version\<close>
 
 theory HLog
   imports HTranscendental
 begin
-
-
-(* should be in NSA.ML *)
-lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
-  by (simp add: epsilon_def star_n_zero_num star_n_le)
-
-lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
-  by auto
-
 
 definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
   where [transfer_unfold]: "x powhr a = starfun2 (powr) x a"
 
 definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"

   by transfer simp
 
 lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
   by transfer simp
 
-lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
+lemma powhr_divide: "\<And>a x y. 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
   by transfer (rule powr_divide)
 
 lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
   by transfer (rule powr_add)