Nicolas Méric 2b1a9d009e Add support invariants on attributes of attributes ... Support invariants on attributes of classes atttributes. Example: doc_class inv_test1 = a :: int doc_class inv_test2 = b :: "inv_test1" c:: int invariant inv_test2 :: "c σ = 1" invariant inv_test2' :: "a (b σ) = 2" doc_class inv_test3 = inv_test1 + b :: "inv_test1" c:: int invariant inv_test3 :: "a σ = 1" invariant inv_test3' :: "a (b σ) = 2" To support invariant on attributes in attributes and invariant on attributes of the superclasses, we check that the type of the attribute of the subclass is ground:› ML‹ val Type(st, [ty]) = \<^typ>‹inv_test1› val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme› val t = ty = \<^typ>‹unit› ›		2023-01-13 08:27:26 +01:00
..
DOF	Add support invariants on attributes of attributes	2023-01-13 08:27:26 +01:00
document-templates	clarified DOF.options: hard-wired document_comment_latex always uses LaTeX version of comment.sty	2022-12-01 21:30:32 +01:00
ontologies	Comment out hack for Assumption in scholarly_paper	2022-12-22 09:55:46 +01:00
scala	Tuned messages, following Isabelle/d6a2a8bc40e1	2022-12-05 15:21:26 +01:00
tests	Add support invariants on attributes of attributes	2023-01-13 08:27:26 +01:00
ROOT	Add missing file (amending 5471d873a9)	2022-12-04 19:26:28 +01:00
ROOTS	Fixed file attributes.	2022-04-18 09:20:36 +01:00