changeset 14427 | cea7d2f76112 |
parent 14418 | b62323c85134 |
child 14464 | 72ad5f2a3803 |
--- a/NEWS Tue Mar 02 11:06:37 2004 +0100 +++ b/NEWS Wed Mar 03 22:58:23 2004 +0100 @@ -109,6 +109,8 @@ the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). + - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. + EX x. x = sel r to True (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. * 'specification' command added, allowing for definition by