equal
deleted
inserted
replaced
6 |
6 |
7 Set = Ord + |
7 Set = Ord + |
8 |
8 |
9 |
9 |
10 (** Core syntax **) |
10 (** Core syntax **) |
|
11 |
|
12 global |
11 |
13 |
12 types |
14 types |
13 'a set |
15 'a set |
14 |
16 |
15 arities |
17 arities |
119 |
121 |
120 |
122 |
121 |
123 |
122 (** Rules and definitions **) |
124 (** Rules and definitions **) |
123 |
125 |
|
126 local |
|
127 |
124 rules |
128 rules |
125 |
129 |
126 (* Isomorphisms between Predicates and Sets *) |
130 (* Isomorphisms between Predicates and Sets *) |
127 |
131 |
128 mem_Collect_eq "(a : {x. P(x)}) = P(a)" |
132 mem_Collect_eq "(a : {x. P(x)}) = P(a)" |