diff -r c23ded11158f -r bc10bb8d0809 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed May 09 00:33:12 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed May 09 00:57:46 2007 +0200
@@ -149,6 +149,11 @@
    hnorm (inverse a) = inverse (hnorm a)"
 by transfer (rule norm_inverse)
 
+lemma hnorm_divide:
+  "\<And>a b::'a::{real_normed_field,division_by_zero} star.
+   hnorm (a / b) = hnorm a / hnorm b"
+by transfer (rule norm_divide)
+
 lemma hypreal_hnorm_def [simp]:
   "\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>"
 by transfer (rule real_norm_def)