| changeset 12937 | 0c4fd7529467 |
| parent 12897 | f4d10ad0ea7b |
| child 13103 | 66659a4b16f6 |
--- a/src/HOL/Set.thy Mon Feb 25 20:46:09 2002 +0100 +++ b/src/HOL/Set.thy Mon Feb 25 20:48:14 2002 +0100 @@ -212,7 +212,7 @@ lemma CollectD: "a : {x. P(x)} ==> P(a)" by simp -lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B" +lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B" apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals]) apply (rule Collect_mem_eq) apply (rule Collect_mem_eq)