equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle release |
4 New in this Isabelle release |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Provers/linorder: New generic prover for transitivity reasoning over |
|
10 linear orders. Note: this prover is not efficient! |
8 |
11 |
9 * Provers/simplifier: |
12 * Provers/simplifier: |
10 |
13 |
11 - Completely reimplemented Asm_full_simp_tac: |
14 - Completely reimplemented Asm_full_simp_tac: |
12 Assumptions are now subject to complete mutual simplification, |
15 Assumptions are now subject to complete mutual simplification, |
84 * Isar: preview of problems to finish 'show' now produce an error |
87 * Isar: preview of problems to finish 'show' now produce an error |
85 rather than just a warning (in interactive mode); |
88 rather than just a warning (in interactive mode); |
86 |
89 |
87 |
90 |
88 *** HOL *** |
91 *** HOL *** |
|
92 |
|
93 * New tactic "trans_tac" and method "trans" instantiate |
|
94 Provers/linorder.ML for axclasses "order" and "linorder" (predicates |
|
95 "<=", "<" and "="). |
89 |
96 |
90 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main |
97 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main |
91 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; |
98 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; |
92 |
99 |
93 * 'typedef' command has new option "open" to suppress the set |
100 * 'typedef' command has new option "open" to suppress the set |