| changeset 4347 | d683b7898c61 |
| parent 3837 | d7f033c74b38 |
| child 17456 | bcf7544875b2 |
| 4346:15fab62268c3 | 4347:d683b7898c61 |
|---|---|
118 "(a : {x. P(x)}) <-> P(a)" ]); |
118 "(a : {x. P(x)}) <-> P(a)" ]); |
119 |
119 |
120 val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong]; |
120 val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong]; |
121 |
121 |
122 val set_ss = FOL_ss addcongs set_congs |
122 val set_ss = FOL_ss addcongs set_congs |
123 delsimps (ex_simps @ all_simps) (*NO miniscoping*) |
|
124 addsimps mem_rews; |
123 addsimps mem_rews; |