From 4f8e5881383e960c3ed6c07888a34601834b1c0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Wed, 24 May 2023 14:17:16 +0200
Subject: [PATCH] Document disable_assert_evaluation theory atttribute in the
 manual

---
 Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy | 3 ++-
 Isabelle_DOF/thys/manual/M_04_RefMan.thy           | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy
index 027d6b9..b1cb58e 100644
--- a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy
+++ b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy
@@ -232,7 +232,8 @@ assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.s
         \<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
 
 text\<open>
-Evaluation of \<open>assert*\<close> can be disabled using the *\<open>disable_assert_evaluation\<close> theory attribute.
+The evaluation of @{command "assert*"} can be disabled
+using the *\<open>disable_assert_evaluation\<close> theory attribute.
 Then only the checking of the term is done:
 \<close>
 declare[[disable_assert_evaluation]]
diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy
index 541735d..3a398e9 100644
--- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy
+++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy
@@ -520,6 +520,11 @@ The @{command "assert*"}-command allows for logical statements to be checked in
 % TODO:
 % Section reference @{docitem (unchecked) \<open>text-elements-expls\<close>} has not the right number
 This is particularly useful to explore formal definitions wrt. their border cases.
+For @{command "assert*"}, the evaluation of the term can be disabled
+with the \<^boxed_theory_text>\<open>disable_assert_evaluation\<close> theory attribute:
+  @{boxed_theory_text [display]\<open>
+  declare[[disable_assert_evaluation]]\<close>}
+Then @{command "assert*"} will act like @{command "term*"}.
 
 The @{command "definition*"}-command allows \<open>prop\<close>, \<open>spec_prems\<close>, and \<open>for_fixes\<close>
 (see the @{command "definition"} command in @{cite "wenzel:isabelle-isar:2020"}) to contain