| changeset 3469 | 61d927bd57ec |
| parent 3420 | 02dc9c5b035f |
| child 3582 | b87c86b6c291 |
| 3468:1f972dc8eafb | 3469:61d927bd57ec |
|---|---|
8 |
8 |
9 open Set; |
9 open Set; |
10 |
10 |
11 section "Relating predicates and sets"; |
11 section "Relating predicates and sets"; |
12 |
12 |
13 AddIffs [mem_Collect_eq]; |
13 Addsimps [Collect_mem_eq]; |
14 AddIffs [mem_Collect_eq]; |
|
14 |
15 |
15 goal Set.thy "!!a. P(a) ==> a : {x.P(x)}"; |
16 goal Set.thy "!!a. P(a) ==> a : {x.P(x)}"; |
16 by (Asm_simp_tac 1); |
17 by (Asm_simp_tac 1); |
17 qed "CollectI"; |
18 qed "CollectI"; |
18 |
19 |