equal
deleted
inserted
replaced
355 by (simp add: HFinite_def) 
355 by (simp add: HFinite_def) 
356 
356 
357 lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)" 
357 lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)" 
358 by (simp add: HFinite_def) 
358 by (simp add: HFinite_def) 
359 
359 
360 lemma HFinite_hnorm_iff [iff]: "(hnorm x \<in> HFinite) = (x \<in> HFinite)" 
360 lemma HFinite_hnorm_iff [iff]: 

361 "(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)" 
361 by (simp add: HFinite_def) 
362 by (simp add: HFinite_def) 
362 
363 
363 lemma HFinite_number_of [simp]: "number_of w \<in> HFinite" 
364 lemma HFinite_number_of [simp]: "number_of w \<in> HFinite" 
364 by (unfold star_number_def, rule HFinite_star_of) 
365 by (unfold star_number_def, rule HFinite_star_of) 
365 
366 