equal
deleted
inserted
replaced
54 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
54 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
55 (Isar) contexts. |
55 (Isar) contexts. |
56 |
56 |
57 *** HOL *** |
57 *** HOL *** |
58 |
58 |
|
59 * Records: |
|
60 - Record types are now by default printed with their type abbreviation |
|
61 instead of the list of all field types. This can be configured via |
|
62 the reference "print_record_type_abbr". |
|
63 - Simproc "record_upd_simproc" for simplification of multiple updates added |
|
64 (not enabled by default). |
|
65 - Tactic "record_split_simp_tac" to split and simplify records added. |
|
66 |
59 * 'specification' command added, allowing for definition by |
67 * 'specification' command added, allowing for definition by |
60 specification. There is also an 'ax_specification' command that |
68 specification. There is also an 'ax_specification' command that |
61 introduces the new constants axiomatically. |
69 introduces the new constants axiomatically. |
62 |
70 |
63 * SET-Protocol: formalization and verification of the SET protocol suite; |
71 * SET-Protocol: formalization and verification of the SET protocol suite; |