equal
deleted
inserted
replaced
55 * Isabelle/Isar reference manual provides more formal references in |
55 * Isabelle/Isar reference manual provides more formal references in |
56 syntax diagrams. |
56 syntax diagrams. |
57 |
57 |
58 |
58 |
59 *** HOL *** |
59 *** HOL *** |
|
60 |
|
61 * Finite_Set.thy: locale fun_left_comm uses point-free characterisation; |
|
62 interpretation proofs may need adjustment. INCOMPATIBILITY. |
60 |
63 |
61 * Nitpick: |
64 * Nitpick: |
62 - Added "need" and "total_consts" options. |
65 - Added "need" and "total_consts" options. |
63 - Reintroduced "show_skolems" option by popular demand. |
66 - Reintroduced "show_skolems" option by popular demand. |
64 - Renamed attribute: nitpick_def ~> nitpick_unfold. |
67 - Renamed attribute: nitpick_def ~> nitpick_unfold. |