--- a/src/Doc/Functions/Functions.thy Tue May 21 11:47:11 2019 +0200
+++ b/src/Doc/Functions/Functions.thy Tue May 21 11:30:30 2019 +0200
@@ -347,6 +347,15 @@
method a bit stronger: it can then use multiset orders internally.
\<close>
+subsection \<open>Configuring simplification rules for termination proofs\<close>
+
+text \<open>
+ Since both \<open>lexicographic_order\<close> and \<open>size_change\<close> rely on the simplifier internally,
+ there can sometimes be the need for adding additional simp rules to them.
+ This can be done either as arguments to the methods themselves, or globally via the
+ theorem attribute \<open>termination_simp\<close>, which is useful in rare cases.
+\<close>
+
section \<open>Mutual Recursion\<close>
text \<open>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Tue May 21 11:47:11 2019 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Tue May 21 11:30:30 2019 +0200
@@ -489,6 +489,7 @@
@{method_def (HOL) relation} & : & \<open>method\<close> \\
@{method_def (HOL) lexicographic_order} & : & \<open>method\<close> \\
@{method_def (HOL) size_change} & : & \<open>method\<close> \\
+ @{attribute_def (HOL) termination_simp} & : & \<open>attribute\<close> \\
@{method_def (HOL) induction_schema} & : & \<open>method\<close> \\
\end{matharray}
@@ -535,6 +536,10 @@
For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
(as for @{method auto}).
+ \<^descr> @{attribute (HOL) termination_simp} declares extra rules for the
+ simplifier, when invoked in termination proofs. This can be useful, e.g.,
+ for special rules involving size estimations.
+
\<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
from well-founded induction and completeness of patterns. This factors out
some operations that are done internally by the function package and makes