--- 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