From 9603311a9aa81e8291e94625dcf640a0e39a6dbb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Fri, 1 Apr 2022 09:54:16 +0200
Subject: [PATCH] Fix DOF manual and tests to work with assert*

---
 .../Isabelle_DOF-Manual/04_RefMan.thy                 |  7 ++++---
 src/tests/AssnsLemmaThmEtc.thy                        | 11 ++++++++---
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
index 31fc481..56646ed 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
@@ -707,9 +707,10 @@ author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
 \<close>
 
 text\<open>Assertions allow for logical statements to be checked in the global context.
-This is particularly useful to explore formal definitions wrt. their border cases. \<close>
-
-assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>
+This is particularly useful to explore formal definitions wrt. their border cases.
+@{boxed_theory_text [display]\<open>
+assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>\<close>}
+\<close>
 
 text\<open>We want to check the consequences of this definition and can add the following statements:
 @{boxed_theory_text [display]\<open>
diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy
index 299c7d6..b9d216d 100755
--- a/src/tests/AssnsLemmaThmEtc.thy
+++ b/src/tests/AssnsLemmaThmEtc.thy
@@ -29,10 +29,15 @@ print_doc_items
 
 section\<open>Definitions, Lemmas, Theorems, Assertions\<close>
 
-
+term\<open>True\<close>
 text*[aa::F, properties = "[@{term ''True''}]"]
 \<open>Our definition of the HOL-Logic has the following properties:\<close>
-assert*[aa::F] "True"
+assert*\<open>F.properties @{F \<open>aa\<close>} = [@{term ''True''}]\<close>
+
+text\<open>For now, as the term annotation is not bound to a meta logic which will translate
+\<^term>\<open>[@{term ''True''}]\<close> to \<^term>\<open>[True]\<close>, we can not use the HOL \<^const>\<open>True\<close> constant
+in the assertion.
+\<close>
 
 (* does not work in batch mode ... 
 (* sample for accessing a property filled with previous assert's of "aa" *)
@@ -70,7 +75,7 @@ different class. "F" and "assertion" have only in common that they posses the at
 
 text\<open>Creation just like that: \<close>
 assert*[ababa::assertion] "3 < (4::int)"
-assert*[ababa::assertion] "0 < (4::int)"
+assert*[ababab::assertion] "0 < (4::int)"
 
 
 end