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/Hyperreal/HLog.thy
changeset 21404 eb85850d3eb7
parent 19765 dfe940911617
child 27435 b3f8e9bdf9a7 
--- a/src/HOL/Hyperreal/HLog.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/HLog.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -19,10 +19,11 @@
 
 
 definition
-  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
+  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
   "x powhr a = starfun2 (op powr) x a"
   
-  hlog :: "[hypreal,hypreal] => hypreal"
+definition
+  hlog :: "[hypreal,hypreal] => hypreal" where
   "hlog a x = starfun2 log a x"
 
 declare powhr_def [transfer_unfold]
isabelle