changeset 14565 | c6dc17aab88a |
parent 14477 | cc61fd03e589 |
child 14658 | b1293d0f8d5f |
--- a/src/HOL/Hyperreal/HyperDef.thy Wed Apr 14 13:28:46 2004 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Wed Apr 14 14:13:05 2004 +0200 @@ -68,6 +68,10 @@ omega :: hypreal ("\<omega>") epsilon :: hypreal ("\<epsilon>") +syntax (HTML output) + omega :: hypreal ("\<omega>") + epsilon :: hypreal ("\<epsilon>") + defs (overloaded)