src/HOL/Real/HahnBanach/Linearform.thy
changeset 25762 c03e9d04b3e4
parent 23378 1d138d6bb461
child 27611 2c01c0bdb385
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jan 02 12:22:38 2008 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Wed Jan 02 15:14:02 2008 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4  *}
     1.5  
     1.6  locale linearform = var V + var f +
     1.7 +  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
     1.8    assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     1.9      and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
    1.10