Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix type of hnorm
authorhuffman
Fri, 05 Jun 2009 00:24:47 -0700
changeset 31449 27e00c983b7b
parent 31448 29090e3111bd
child 31450 d0ffa8fad5bb
fix type of hnorm
src/HOL/NSA/NSA.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle