equal
deleted
inserted
replaced
87 * Isar: preview of problems to finish 'show' now produce an error |
87 * Isar: preview of problems to finish 'show' now produce an error |
88 rather than just a warning (in interactive mode); |
88 rather than just a warning (in interactive mode); |
89 |
89 |
90 |
90 |
91 *** HOL *** |
91 *** HOL *** |
|
92 |
|
93 * GroupTheory: new, experimental summation operator for abelian groups. |
92 |
94 |
93 * New tactic "trans_tac" and method "trans" instantiate |
95 * New tactic "trans_tac" and method "trans" instantiate |
94 Provers/linorder.ML for axclasses "order" and "linorder" (predicates |
96 Provers/linorder.ML for axclasses "order" and "linorder" (predicates |
95 "<=", "<" and "="). |
97 "<=", "<" and "="). |
96 |
98 |