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