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