From e4e8199e337ab32233358bb74b9e7d1998da1677 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Thu, 21 Apr 2022 11:14:32 +0200
Subject: [PATCH] Explain disabled invariant in SWIS_E

---
 examples/scholarly_paper/2021-ITP-PMTI/paper.thy | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
index 80544ff..956f04f 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
+++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
@@ -1037,6 +1037,9 @@ doc_class cenelec_document = text_element +
    invariant two_eyes_prcple :: "written_by \<sigma> \<noteq> fst_check \<sigma> 
                                      \<and> written_by \<sigma> \<noteq> snd_check \<sigma>"
 
+(* artificial definition to enable checking in text\<open>\<close>
+   It will have to be implemented to enable the invariant well_formed_pre in SWIS_E.
+*)
 definition "iswff\<^sub>p\<^sub>r\<^sub>e" :: "bool" 
   where "iswff\<^sub>p\<^sub>r\<^sub>e \<equiv> True"
 
@@ -1045,6 +1048,7 @@ doc_class SWIS_E =
    op_args_res       :: "(string \<times> typ) list \<times> typ" \<comment> \<open>args and result type\<close>
    pre_cond          :: "(string \<times> thm) list"        \<comment> \<open>labels and predicates\<close>
    post_cond         :: "(string \<times> thm) list"        \<comment> \<open>labels and predicates\<close>
+  (* iswff\<^sub>p\<^sub>r\<^sub>e  will have to be implemented to enable the invariant well_formed_pre. *)
   (* invariant well_formed_pre :: "\<forall>cond \<in> set(map snd (pre_cond \<sigma>)). 
                                               iswff\<^sub>p\<^sub>r\<^sub>e (op_args_res \<sigma>) (cond)"
    invariant well_formed_post:: ...*)