Theorem_default_class theory attribute does not override Definition_default_class theory attribute #11

New Issue

nicolas.meric · 2022-03-22T16:05:43Z

nicolas.meric commented

2022-03-22 16:05:43 +00:00

Test to do in a theory which imports \<^theory>‹Isabelle_DOF.CENELEC_50128› and \<^theory>‹Isabelle_DOF.scholarly_paper›.

\<^theory>‹Isabelle_DOF.CENELEC_50128› declares:

declare[[ Definition_default_class="semi_formal_content"]]

Example in a test theory:

declare[[ Theorem_default_class = scholarly_paper.theorem]]
Theorem*[T1444444::"theorem", short_name="‹DF definition captures deadlock-freeness›"]  ‹ … ›
print_doc_items

Fails with the message:
class scholarly_paper.theorem must be sub-class of CENELEC_50128.semi_formal_content

Test to do in a theory which imports \\<^theory>‹Isabelle_DOF.CENELEC_50128› and \\<^theory>‹Isabelle_DOF.scholarly_paper›. \\<^theory>‹Isabelle_DOF.CENELEC_50128› declares: ``` declare[[ Definition_default_class="semi_formal_content"]] ``` Example in a test theory: ``` declare[[ Theorem_default_class = scholarly_paper.theorem]] Theorem*[T1444444::"theorem", short_name="‹DF definition captures deadlock-freeness›"] ‹ … › print_doc_items ``` Fails with the message: class scholarly_paper.theorem must be sub-class of CENELEC_50128.semi_formal_content

nicolas.meric referenced this issue from a commit

2022-04-08 10:17:57 +00:00

Fix {Theorem, Lemma}_default_class theory attributes

nicolas.meric closed this issue

2022-04-08 10:17:57 +00:00

Sign in to join this conversation.