| changeset 458 | 877704b91847 |
| parent 456 | f1df7fc211a7 |
| child 479 | db5a95f2952e |
| 457:8577bc1c4e1b | 458:877704b91847 |
|---|---|
21 should be addsimps |
21 should be addsimps |
22 |
22 |
23 Ref/tactic: documented subgoals_tac |
23 Ref/tactic: documented subgoals_tac |
24 |
24 |
25 Logics/ZF: renamed mem_anti_sym and mem_anti_refl |
25 Logics/ZF: renamed mem_anti_sym and mem_anti_refl |
26 |
|
27 Ref/defining: type constraints ("::") now have a very low priority of 4. |
|
28 As in ML, they must be enclosed in paretheses most of the time. |