From a68ecb4f112a6b7b5bfb92bb95e2638c3903f2c0 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Thu, 31 Mar 2022 10:12:46 +0200
Subject: [PATCH] ...

---
 src/tests/Evaluation.thy | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/tests/Evaluation.thy b/src/tests/Evaluation.thy
index e1bdf02..7d88a5c 100644
--- a/src/tests/Evaluation.thy
+++ b/src/tests/Evaluation.thy
@@ -62,13 +62,11 @@ text\<open>Now we can evaluate a term with TA:
 the current implementation return the term which references the object referenced by the TA.
 Here the evualuation of the TA will return the HOL.String which references the theorem:
 \<close>
-value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
+value*\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>syntax check\<close>
 
-value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
+value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>defining a reference of class A\<close> 
 
-value*[axxxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
-
-text\<open>check : @{A [display] "axxx"}\<close>
+text\<open>check : @{A [display] "axxx"}\<close> \<comment> \<open>using it\<close> 
 
 text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
 It is a concept which will be used to implement an ontology. It has roughly the same meaning as