# HG changeset patch
# User huffman
# Date 1244186687 25200
# Node ID 27e00c983b7bce34bf2df0d9691d016ebc699b10
# Parent  29090e3111bd5cd3bb599a2f934f77d37a37020b
fix type of hnorm

diff -r 29090e3111bd -r 27e00c983b7b src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Jun 04 17:28:31 2009 -0700
+++ b/src/HOL/NSA/NSA.thy	Fri Jun 05 00:24:47 2009 -0700
@@ -12,7 +12,7 @@
 begin
 
 definition
-  hnorm :: "'a::norm star \<Rightarrow> real star" where
+  hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" where
   [transfer_unfold]: "hnorm = *f* norm"
 
 definition