src/HOL/Hyperreal/NSA.thy
changeset 14565 c6dc17aab88a
parent 14477 cc61fd03e589
child 14653 0848ab6fe5fc
     1.1 --- a/src/HOL/Hyperreal/NSA.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -43,6 +43,9 @@
     1.4  syntax (xsymbols)
     1.5      approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +    approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
     1.9 +
    1.10  
    1.11  
    1.12  subsection{*Closure Laws for  Standard Reals*}