--- a/CONTRIBUTORS Fri Sep 02 23:41:54 2022 +0200
+++ b/CONTRIBUTORS Fri Sep 02 23:42:09 2022 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* August 2022: Norbert Schirmer, Apple
+ Record simproc that sorts update expressions.
+
* June 2022: Jan van Brügge, TU München
Strict cardinality bounds for BNFs.
--- a/NEWS Fri Sep 02 23:41:54 2022 +0200
+++ b/NEWS Fri Sep 02 23:42:09 2022 +0200
@@ -66,6 +66,10 @@
*** HOL ***
+* HOL record: new simproc that sorts update expressions, guarded by
+configuration option "record_sort_updates" (default: false). Some
+examples are in theory "HOL-Examples.Records".
+
* HOL-Algebra: Facts renamed to avoid fact name clashes on interpretation:
is_ring ~> ring_axioms