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/Subspace.thy
changeset 10606 e3229a37d53f
parent 10309 a7f961fb62c6
child 10687 c186279eecea 
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Dec 06 12:28:52 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Dec 06 12:34:12 2000 +0100
@@ -382,9 +382,9 @@
             assume "a = (#0::real)" show ?thesis by (simp!)
           next
             assume "a \<noteq> (#0::real)" 
-            from h have "rinv a \<cdot> a \<cdot> x' \<in> H" 
+            from h have "inverse a \<cdot> a \<cdot> x' \<in> H" 
               by (rule subspace_mult_closed) (simp!)
-            also have "rinv a \<cdot> a \<cdot> x' = x'" by (simp!)
+            also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!)
             finally have "x' \<in> H" .
             thus ?thesis by contradiction
           qed
isabelle