src/HOL/Set.thy
changeset 25502 9200b36280c0
parent 25460 b80087af2274
child 25510 38c15efe603b
     1.1 --- a/src/HOL/Set.thy	Thu Nov 29 07:55:46 2007 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Nov 29 17:08:26 2007 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4  
     1.5  instance set :: (type) ord
     1.6    subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
     1.7 -  psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
     1.8 +  psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
     1.9  lemmas [code func del] = subset_def psubset_def
    1.10  
    1.11  abbreviation