Mercurial Mercurial > repos > isabelle / diff
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/Complex/NSCA.thy
changeset 20557 81dd3679f92c
parent 20552 2c31dd358c21
child 20559 2116b7a371c7 
--- a/src/HOL/Complex/NSCA.thy	Sat Sep 16 19:14:37 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy	Sat Sep 16 23:46:38 2006 +0200
@@ -1119,7 +1119,8 @@
 
 lemma SComplex_SReal_hcomplex_of_hypreal:
      "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
-by (auto simp add: SReal_def SComplex_def hcomplex_of_hypreal_def)
+by (auto simp add: SReal_def SComplex_def hcomplex_of_hypreal_def
+         simp del: star_of_of_real)
 
 lemma stc_hcomplex_of_hypreal: 
  "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
isabelle