equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Set theory for higher-order logic. A set is simply a predicate. |
6 Set theory for higher-order logic. A set is simply a predicate. |
7 *) |
7 *) |
8 |
|
9 open Set; |
|
10 |
8 |
11 section "Relating predicates and sets"; |
9 section "Relating predicates and sets"; |
12 |
10 |
13 Addsimps [Collect_mem_eq]; |
11 Addsimps [Collect_mem_eq]; |
14 AddIffs [mem_Collect_eq]; |
12 AddIffs [mem_Collect_eq]; |