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/Multivariate_Analysis/Bounded_Continuous_Function.thy
changeset 61169 4de9ff3ea29a
parent 60421 92d9557fb78c
child 61260 e6f03fae14d5 
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -315,7 +315,7 @@
   by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
 
 instance
-  by default
+  by standard
     (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
       Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
       plus_cont const_bcontfun minus_cont scaleR_cont)
isabelle