| changeset 61378 | 3e04c9ca001a |
| parent 61284 | 2314c2f62eb1 |
| child 61609 | 77b453bd616f |
--- a/src/HOL/NSA/NSA.thy Fri Oct 09 19:51:20 2015 +0200 +++ b/src/HOL/NSA/NSA.thy Fri Oct 09 20:26:03 2015 +0200 @@ -46,9 +46,6 @@ notation (xsymbols) approx (infixl "\<approx>" 50) -notation (HTML output) - approx (infixl "\<approx>" 50) - lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}" by (simp add: Reals_def image_def)