NEWS
changeset 77955 c4677a6aae2c
parent 77915 64beebac04b8
child 77991 bdb5de00379a
--- a/NEWS	Tue May 02 14:19:34 2023 +0200
+++ b/NEWS	Tue May 02 19:49:17 2023 +0200
@@ -7,6 +7,17 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* The special "of_class" introduction rule for 'class' definitions has
+been renamed from "class.NAME.of_class.intro" to "NAME.intro_of_class"
+(where NAME is the name specification of the class). E.g. see the HOL
+library:
+
+  class.preorder.of_class.intro  ~>  preorder.intro_of_class
+  class.order.of_class.intro  ~> order.intro_of_class
+
+
 *** Document preparation ***
 
 * Various well-known LaTeX styles are included as Isabelle components,