Mercurial Mercurial > repos > testboard / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/NSA.thy
changeset 20562 c2f672be8522
parent 20554 c433e78d4203
child 20563 44eda2314aab
equal deleted inserted replaced
20561:6a6d8004322f 20562:c2f672be8522 
   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
testboard