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/Real/HahnBanach/HahnBanach.thy
changeset 19984 29bb4659f80a
parent 19931 fb32b43e7f80
child 23378 1d138d6bb461 
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 04 14:47:01 2006 +0200
@@ -334,10 +334,10 @@
      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
-  have E: "vectorspace E" by intro_locales
-  have E_norm: "normed_vectorspace E norm" by rule intro_locales
+  have E: "vectorspace E" by unfold_locales
+  have E_norm: "normed_vectorspace E norm" by rule unfold_locales
   have FE: "F \<unlhd> E" .
-  have F: "vectorspace F" by rule intro_locales
+  have F: "vectorspace F" by rule unfold_locales
   have linearform: "linearform F f" .
   have F_norm: "normed_vectorspace F norm"
     by (rule subspace_normed_vs)
isabelle