diff -r 3f2c371a3de9 -r e6f026505c5b src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed Aug 14 18:59:49 2024 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Aug 14 21:23:22 2024 +0200
@@ -803,12 +803,14 @@
   \end{matharray}
 
   \<^rail>\<open>
-    @{syntax_def simproc_setup}: (@'passive')? @{syntax name}
+    @{syntax_def simproc_setup}: (@'passive')? proc_kind? @{syntax name}
       patterns '=' @{syntax embedded}
     ;
     @{syntax_def simproc_setup_id}:
       @{syntax simproc_setup} (@'identifier' @{syntax thms})?
     ;
+    proc_kind: @'congproc' | @'weak_congproc'
+    ;
     patterns: '(' (@{syntax term} + '|') ')'
     ;
     @@{command simproc_setup} @{syntax simproc_setup}
@@ -836,6 +838,10 @@
   thus \<^emph>\<open>active\<close>. The keyword \<^theory_text>\<open>passive\<close> avoids that: it merely defines a
   simproc that can be activated in a different context later on.
 
+  Regular simprocs produce rewrite rules on the fly, but it is also possible
+  to congruence rules via the @{syntax proc_kind} keywords: \<^theory_text>\<open>congproc\<close> or
+  \<^theory_text>\<open>weak_congproc\<close>.
+
   \<^descr> ML antiquotation @{ML_antiquotation_ref simproc_setup} is like command
   @{command simproc_setup}, with slightly extended syntax following @{syntax
   simproc_setup_id}. It allows to introduce a new simproc conveniently within