src/HOL/Multivariate_Analysis/Euclidean_Space.thy

 
 definition 
   [simp]: "Basis = {1::real}"
 
 instance
-  by default auto
+  by standard auto
 
 end
 
 lemma DIM_real[simp]: "DIM(real) = 1"
   by simp

 
 definition Basis_complex_def:
   "Basis = {1, ii}"
 
 instance
-  by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
+  by standard (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
 
 end
 
 lemma DIM_complex[simp]: "DIM(complex) = 2"
   unfolding Basis_complex_def by simp