# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1602930723 -3600
# Node ID 2dd41a8893aaa28fbb1ebf82d67a3842e2371fec
# Parent  18e760349b86d3bb1a452efea48db8a8a4ed3782
type class reduction

diff -r 18e760349b86 -r 2dd41a8893aa src/HOL/Analysis/Affine.thy
--- a/src/HOL/Analysis/Affine.thy	Fri Oct 16 21:27:46 2020 +0100
+++ b/src/HOL/Analysis/Affine.thy	Sat Oct 17 11:32:03 2020 +0100
@@ -1008,7 +1008,7 @@
   using affine_hull_span_gen[of "0" S] assms by auto
 
 lemma extend_to_affine_basis_nonempty:
-  fixes S V :: "'n::euclidean_space set"
+  fixes S V :: "'n::real_vector set"
   assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
   shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
 proof -
@@ -1044,7 +1044,7 @@
 qed
 
 lemma affine_basis_exists:
-  fixes V :: "'n::euclidean_space set"
+  fixes V :: "'n::real_vector set"
   shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
 proof (cases "V = {}")
   case True
@@ -1059,7 +1059,7 @@
 qed
 
 proposition extend_to_affine_basis:
-  fixes S V :: "'n::euclidean_space set"
+  fixes S V :: "'n::real_vector set"
   assumes "\<not> affine_dependent S" "S \<subseteq> V"
   obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
 proof (cases "S = {}")
@@ -1258,7 +1258,9 @@
   shows "aff_dim {a} = 0"
   using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto
 
-lemma aff_dim_2 [simp]: "aff_dim {a,b} = (if a = b then 0 else 1)"
+lemma aff_dim_2 [simp]:
+  fixes a :: "'n::euclidean_space"
+  shows "aff_dim {a,b} = (if a = b then 0 else 1)"
 proof (clarsimp)
   assume "a \<noteq> b"
   then have "aff_dim{a,b} = card{a,b} - 1"